The 5th Joint Seminar on Programming Languages and Systems


第五次程式語言暨系統研討會

Sponsored by
Institute of Information Science, Academia Sinica


中央研究院 資訊科學研究所

December 17, 2003


Schedule

10:00 -- 10:50
Register Allocation by Proof Transformation
Atsushi Ohori, Japan Advanced Institute of Science and Technology
11:00 -- 11:50
Probabilistic Point-to Analysis for Speculative Program Executions
李政崑 清華大學 資訊工程學系 (Jenq Kuen Lee, National Tsing Hua University)
13:30 -- 14:20
Composition, Decomposition, and Refinement of Temporal-Logic Specifications
蔡益坤 台灣大學 資訊管理學系 (Yih-Kuen Tsay, National Taiwan University)
14:30 -- 15:20
Implementing Visitor Pattern in O'Caml --- A Case Study
王柏堯 中央研究院 資訊科學研究所 (Bow-Yaw Wang, Academia Sinica)
 

Purposes


This seminar series aims to bring together researchers and students working on programming languages and systems to present results in their fields. It hopes to provide a stimulating environment to further facilitate the exchange of ideas and experiences among the participants.


Further Information

The seminar will be held at 台北市 南港區 中央研究院 資訊科學研究所 106 會議室 on December 17 (Wednesday), 2003.
Direction to the seminar location is available at http://www.sinica.edu.tw/as/map/index_c.html

Students are especially welcomed to attend this seminar series. There is no registration fee and lunches will be provided. To help plan the event, however, please send a plain text e-mail to trc@iis.sinica.edu.tw with your name and current affiliation if you plan to attend.

Further information about this event, including abstracts of the talks, is available from WWW at http://www.iis.sinica.edu.tw/~trc/plas2003.html


Abstracts

Register Allocation by Proof Transformation

Atsushi Ohori, Japan Advanced Institute of Science and Technology.

This paper presents a proof-theoretical framework that accounts for the entire process of register allocation -- liveness analysis is proof reconstruction (similar to type inference), and register allocation is proof transformation from a proof system with unrestricted variable accesses to a proof system with restricted variable access. In our framework, the set of registers acts as a ``working set'' of the live variables at each instruction step, which changes during the execution of the code. This eliminates the ad-hoc notion of ``spilling''. Memory-register moves are systematically incorporated in our proof transformation process. Its correctness is a direct corollary of our construction; the resulting proof is equivalent to the proof of the original code modulo treatment of structural rules. The framework serves as a basis for reasoning about formal properties of register allocation process, and it also yields a clean and systematic register allocation algorithm. The algorithm has been implemented, demonstrating the feasibility of the framework.


Probabilistic Point-to Analysis for Speculative Program Executions

李政崑 清華大學 資訊工程學系 (Jenq Kuen Lee, National Tsing Hua University)

Information gathered by the existing pointer analysis techniques can be classified as must aliases or definitely-points-to relationships, which hold for all executions, and may aliases or possibly-points-to relationships, which might hold for some executions. Such information does not provide quantitative descriptions to tell how likely the conditions will hold for the executions, which are needed for modern compiler optimizations, and thus has hindered compilers from more aggressive optimizations. We have addressed this issue by proposing a probabilistic points-to analysis technique to compute the probability of each points-to relationship, and we have applied this technique on speculative program exeuctions on Speculative multithreading (SpMT) architecture.

SpMT can exploit thread-level parallelism that cannot be identified statically. Speedup can be obtained by speculatively executing threads in parallel that are extracted from a sequential program. However, performance degradation might happen if the threads are highly dependent, since a recovery mechanism will be activated when a speculative thread executes incorrectly and such a recovery action usually incur a very high penalty. Therefore, it is essential for SpMT to quantify the degree of dependences and to turn off speculation if the degree of dependences passes certain thresholds. We have developed a technique that quantitatively computes dependences between loop iterations and such information can be used to determine if loop iterations can be executed in parallel by speculative threads. This technique can be broken into two steps. First probabilistic points-to analysis is performed to estimate the probabilities of points-to relationships in case there are pointer references in programs, and then the degree of dependences between loop iterations is computed quantitatively. Preliminary experimental results show compiler-directed thread-level speculation based on the information gathered by this technique can achieve significant performance improvement on SpMT.


Composition, Decomposition, and Refinement of Temporal-Logic Specifications

蔡益坤 台灣大學 資訊管理學系 (Yih-Kuen Tsay, National Taiwan University)

Temporal logic (specifically the Linear-Time Temporal Logic of Manna and Pnueli) is one convenient formalism for specifying and reasoning about reactive systems and their properties. Fundamental concepts in formal verification such as refinement (implementation), hiding, and parallel composition can all be conveniently treated with the logic. In this talk, I will show how to write the specification of a reactive module and to derive properties from a composition of such modules. I will also show how to prove that a concrete composite system implements an abstract composite system by reasoning about their constituent modules.


Implementing Visitor Pattern in O'Caml --- A Case Study

王柏堯 中央研究院 資訊科學研究所 (Bow-Yaw Wang, Academia Sinica)

The visitor pattern is known to be a difficult inheritance problem of inter-related classes. For static-typed languages such as O'Caml, it takes some effort to devise an implementation which is general for practical applications and safe for type checking. In this talk, I will discuss the visitor pattern implementation used in the model checker OMocha and the benefits of using static-typed languages. It would be interesting to see whether the technique could be used for other design patterns.