Bulk Synchronous Parallel ML: Safety and Expressivity
Bulk Synchronous Parallel (BSP) computing is a parallel programming model which uses explicit processes, offers a high degree of abstraction and yet allows portable and predictable performance on a wide variety of architectures. Our BSML (Bulk Synchronous Parallel ML) language can be seen as an algorithmic skeletons language, because only a finite set of operations are parallel, but is different by two main points: (a) our operations are universal for BSP programming and thus allow the implementation of more classical algorithmic skeletons. It is also possible for the programmer to implement additional skeletons. Moreover performance prediction is possible and the associated cost model is the BSP cost model. Those operations are implemented as a library for the functional programming language Objective Caml; (b) the parallel semantics of BSML are formal ones. We have a confluent calculus, a distributed semantics and a parallel abstract machine, each semantics has been proved correct with respect to the previous one.
This talk will present our current research directions:
Term Rewriting with Variable Binding: An Initial Algebra Approach
We present an extension of first-order term rewriting systems, which involves variable binding in the term language. We develop the systems called binding term rewriting systems (BTRSs) in a stepwise manner; firstly we present the term language, then formulate equational logic, and finally define rewrite systems.
The novelty of this development is that we follow an initial algebra approach in an extended notion of Sigma-algebras in various functor categories. These are based on Fiore-Plotkin-Turi's presheaf semantics of variable binding and L\"uth-Ghani's monadic semantics of term rewriting systems. We characterise the terms, equational logic and rewrite systems for BTRSs are initial algebras in suitable categories.
We will also discuss this approach from the viewpoint of datatypes. There is an interesting connection between Fiore-Plotkin-Turi's semantics and Bird-Meertens-Peterson's notion of "nested datatypes" in functional programming. This suggests that term rewriting with variable binding can be seen as an operational semantics on a nested datatype.
A Development Calculus for Specifications
A first order inference system, named R-calculus, is defined to develop the specifications. This system intends to eliminate the laws which is not consistent with user's requirements. The R-calculus consists of the structural rules, an axiom, a cut rule, and the rules for logical connectives. Some examples are given to demonstrate the usage of the R-calculus. Furthermore, the properties regarding reachability and completeness of the R-calculus are formally defined and proved.
Deterministic Second-order Matching and Its application to Program Transformation
We will present a simple but practical class of patterns for second-order matching in the context of automatic program transformation. While higher-order patterns enable us to write simple specification, general second-order matching algorithm generates notorious nondeterministic matches. In the context of unification, the so-called Miller's higher-order matching has a single unification. We extend the Miller's pattern so as to generate a single match while covering a wide class of patterns being especially useful for the transformation of programs in modern programming languages such as Haskell or ML.
While second-order matching is NP-Complete, a several efficient class of pattern has been proposed by imposing constraint on second-order patterns. For example, an algorithm with second-order pattern restricted by a number of free variables in pattern turned to be polynomial. We will compare our linear time matching algorithm with the standard second order matching by Huet and Lang and the efficient matching algorithm by de Moor and Sittampalam or by Regis Curien, Zhenyu Qian and Hui Shi.
The algorithm has been implemented upon the MAG system for transforming functional programs.
Automating the Dependency Pair Method
Developing automatable methods for proving termination of term rewrite systems that resists traditional techniques based on simplification orders has become an active research area in the past few years. The dependency pair method of Arts and Giesl is one of the more popular such methods. However, there are several obstacles that hamper its automation. In this talk we present new ideas to overcome these obstacles. We provide ample numerical data supporting our ideas, which have been implemented in the Tsukuba Termination Tool. We conclude the talk with a demonstration of this tool.
The talk is based on joint work with Nao Hirokawa. No specific knowledge of term rewriting or termination is assumed.
From Top-Down to Bottom-Up
It often occurs that there are two dual approaches to construct a tree: top-down and bottom-up. The top-down approach serves as a straight forward specification, while it is often preferred to build the tree bottom-up if we want to exploit sharing of overlapping sub-trees. In this talk I am going to talk about some on-going research in deriving, or proving, a bottom-up algorithm from its top-down specification.
XML Transformation Language Intended for Stream Processing
This talk is about my recent work on XML transformation language intended for stream processing. Most of XML transformation languages are implemented as tree manipulation where input XML trees are completely stored in memory. These transformations are apt to cause inefficient memory usage. In contrast, XML stream processing can minimize memory usage because it begins to output the transformation result before reading the whole input. However, it is much harder to program XML stream processing than to specify tree manipulation because stream processing programs often require `stateful programming'. XTiSP, an XML transformation language we introduce, solves the complication of XML stream processing by automatically generating a stream processing program from a specification of an XML tree manipulation. The generation method is based on a framework of attribute grammar. XTiSP helps us to obtain XML stream processing program effortlessly.
タイトル 柔軟にプログラムを解釈する図形言語 (OHP, draft)
概要
エンドユーザにとってプログラミングが難しいのは，プログラムを厳密に
記述しなければならないからである．もっと，柔軟に振る舞うことができる
コンピュータの動作原理が求められている．この為には，プログラムの表現法，
解釈法，実行法，それぞれが柔軟である必要がある．
Fuzzy Rewriting (本提案) は，プログラムを書き換えルールによって表現し，
書き換え対象に厳密に一致しなくても適用可能とし，対象とルールとのずれに
応じて，書き換え結果を決める，というコンピュータの動作原理である．これは，
「近さ」を定義することができる対象に対して，動作させることができる．
Viscuit は Fuzzy Rewriting に従って，図形を書き換え，アニメーションの作成
を簡単にした，図形言語である．これは，Fuzzy Rewriting の実証のみならず，
実際の子供たちに使ってもらえるように設計された．厚木フェスティバルに
おいて，子供たちに使用してもらい，簡単なフィードバックを得たので，それも
合わせて報告する．
公衆無線ＬＡＮサービスのためのモバイルミドルウェア
概要 M-Fletz において採用されたモバイルミドルウェアについて，いかにして 安全な通信を実現するための構成法，およびそのWindows上での実装の仕方・困難 について説明する．
Iterative-free program analysis
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 {\tt 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.
汎用連想計算エンジンGETAとその応用
Abstract 汎用連想計算エンジン GETA(a Generic Engine for Transposable Association) は、与えられた任意の類似度の定義に基づき、検索キー文書の類似文書を大規模 な文書データベースから高速に検索する検索エンジンである。また、文書データ ベースでの文書と単語の役割を入れ替えて検索を行うことで、類似単語の検索も 行うことができる。 これらの機能を組み合わせることで、類似文書検索、任意文書からの連想検索、 文書要約、クエリ拡張、類似単語抽出、文書クラスタリングなど文書マイニング システムに欠かせない機能を容易に実現することが可能である。 本発表では、GETAとその応用について、例を交えて説明する。
From Text to Visual (collaboration with Jun Kurabe, Frontage-Razorfish, Inc.)
Abstract The mail reader which we developed at the IPA's Exploratory Software Project (in Japanese, Mito Software Souzo Jigyo, "未踏ソフトウェア創造 事業") in recent two years, has 3 user interfaces, i.e. text mail reader, visual mail reader and visual mail finder. The text mail reader is a common mail reader with the contents summarizer and mail flow analyzer, and the visual mail reader is a graphical based mail reader which represents a mail flow to a relational graph, and the visual mail finder is an information visualizer and a filter for a large amount of mails. In this talk, we present the algorithms of mail flow analyzer and contents summarizer. And we explain and demonstrate this mail reader.
Shape-based Cost Analysis of Skeletal Parallel Programs
Abstract: Although deducing interesting dynamic characteristics of parallel programs (and in particular, run time) is well known to be an intractable problem in the general case, it can be alleviated by placing restrictions upon the programs which can be expressed. By combining language restrictions based on principles of "shape analysis", and "skeletal programming", we produce a completely automated, computation and communication sensitive cost analysis system for an implicitly parallel functional programming language. This builds on earlier work in the area by quantifying communication as well as computation costs, with the former being derived for the Bulk Synchronous Parallel (BSP) model. We present details of our BSP implementation strategy together with an account of the analysis mechanism by which program behaviour information (such as shape and cost) is statically deduced.
On distributed timestamping: algorithms, prototyping, and analysis.
Abstract: Distributed time-stamping methods based on RSA are discussed, and a new combinatorial method is presented for verifying that a time-stamp is correct in the sense it is synthesized only from correct partial time-stamps. The time-complexity of this method is 60 to 10 times smaller than conventional methods in realistic configurations. This method, however, identifies the incorrect partial time-stamp only when there is at most one incorrect partial time-stamp; otherwise it detects only the existence of incorrect partial time-stamps. First, we sketch an distributed algorithm due to Boneh-Franklin for shared generation of RSA keys. Next, a distributed threshold time-stamping method on the basis of Miyazaki-Sakurai-Mogi distributed signing scheme is sketched. Finally, our method for verifying the correctness of time-stamps is presented, with a description of our prototyping of a distributed time-stamping system. (Collaboration with Satoshi Ono and Akira Takura.)
Composing Stack-Attributed Tree Transducers
Abstract: We present a composition method for stack-attributed tree transducers. Stack-attributed tree transducers extend attributed tree transducers with a pushdown stack device for attribute values. Stack-attributed tree transducers are more powerful than attributed tree transducers due to the stack mechanism. We extend an existing composition method for attributed tree transducers to the composition method for stack- attributed tree transducers. The composition method is proved to be correct and to enjoy a closure property. In this talk, we also present a practical application of the composition method, that is an XML stream transformer generator.
Back to ToPS's Home Page