Isao SasanoPh.D. (March 2002, University of Tokyo)Associate Professor, Department of Information Science and Engineering, College of Engineering, Shibaura Institute of Technology Home page in Japanese Our research group |
Author's version: Copyright ©ICST, 2014. This is the author's version of the work. It is posted here by permission of ICST for your personal use. Not for redistribution. The definitive version was published in the ACM digital library.
Author's version: Copyright ©ACM, 2012. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation (PEPM'12), January 23-24, 2012, Philadelphia, Pennsylvania, USA, http://doi.acm.org/10.1145/2103746.2103771.
Abstract Program analysis is the heart of modern compilers. Most control flow analyses are reduced to the problem of finding a fixed point in a certain transition system, and such fixed point is commonly computed through an iterative procedure that repeats tracing until convergence. This paper proposes a new method to analyze programs through recursive graph traversals instead of iterative procedures, based on the fact that most programs (without spaghetti goto) have well-structured control flow graphs, graphs with bounded tree width. Our main techniques are; an algebraic construction of a control flow graph, called SP Term, which enables control flow analysis to be defined in a natural recursive form, and the Optimization Theorem, which enables us to compute optimal solution by dynamic programming. We illustrate our method with two examples; dead code detection and register allocation. Different from the traditional standard iterative solution, our dead code detection is described as a simple combination of bottom-up and top-down traversals on SP Term. Register allocation is more interesting, as it further requires optimality of the result. We show how the Optimization Theorem on SP Terms works to find an optimal register allocation as a certain dynamic programming.
Abstract In existing work on graph algorithms, it is known that a linear time algorithm can be derived mechanically from a logical formula for a class of optimization problems. But this has a serious problem that the derived algorithm has huge constant factor. In this work, we redefine this problem on recursive data structures as a maximum marking problem and propose method for deriving a linear time algorithm for that. In this method, specification is given using recursive functions instead of logical formula, which results in a practical linear time algorithm. This method is mechanical and in fact, based on this deriving method, we make a system which automatically generates a practical linear time algorithm from specification for a maximum marking problem.
Abstract Data mining, which is a technology for obtaining useful knowledge from large database, has been gradually recognized as an important subject. Algorithms for data mining have to be efficient since target database is often huge, and various kinds of efficient algorithms for data mining are individually investigated. This paper shows that an efficient linear time algorithm for mining optimized gain association rules can be systematically derived from a simple specification by reducing it to an instance of the {\it maximum marking problem}. Our approach not only automatically guarantees the correctness of the derived algorithm, but also is easy to derive new algorithms for modification of the problem.
Abstract Program generation has seen an important role in a wide range of software development processes, where effective calculation rules are critical. In this paper, we propose a more general calculation rule for generation of efficient programs for solving maximum marking problems. Easy to use and implement, our new rule gives a significant extension of the rule proposed by Sasano {\em et al.}, allowing multiple kinds of marks as well as more general description of the property of acceptable markings. We illustrate its effectiveness using several interesting problems.
Abstract In this paper we propose a new method for deriving a practical linear-time algorithm from the specification of a maximum-weightsum problem: From the elements of a data structure $x$, find a subset which satisfies a certain property $p$ and whose weightsum is maximum. Previously proposed methods for automatically generating linear-time algorithms are theoretically appealing, but the algorithms generated are hardly useful in practice due to a huge constant factor for space and time. The key points of our approach are to express the property $p$ by a {\em recursive\/} boolean function over the structure $x$ rather than a usual logical predicate and to apply program transformation techniques to reduce the constant factor. We present an {\em optimization theorem}, give a calculational strategy for applying the theorem, and demonstrate the effectiveness of our approach through several nontrivial examples which would be difficult to deal with when using the methods previously available.