ALCOOL

ALCOOL is a static analyzer whose input language, namely the Parallel Automata Meta Language or PAML, is a fragment of the Dijkstra's PV language [6]. PAML comes with a parallel random-access abstract machine (PRAM) based on shared memory following the concurrent read exclusive write convention (CREW).

The geometric model of a PAML program is a mathematical object which, in some sense, generalizes flowcharts [8] and control flow graphs [1] to parallel programs. The main feature of ALCOOL is to produce it.

ALCOOL can deduce several properties of a PAML program from its geometric model like the presence of deadlocks [7] and the factorization into independent PAML programs [2].

The geometric model is built independently from the value analysis. Therefore ALCOOL approach differs from the ones suggested in [3], [4], and [5]. In fact, the geometric model of a PAML program is designed to be used as the control flow structure of the program to analyze.

ALCOOL is entirely written in OCaml. Its developement has been on and off for almost a decade. Though it is pretty advanced now, it still lacks a user-friendly interface and a documentation. We hope we can make its sources available as soon as possible on github.


[1] Allen, F. E. Control Flow Analysis. In Proceedings of a Symposium on Compiler Optimization, pages 1–19. ACM, 1970.
[2] Balabonski, T. and Haucourt, E. A Geometric Approach to the problem of Unique Decomposition of Processes. In Concurrency Theory 21th International Conference, vol. 6269 of Lecture Notes in Computer Science, pages 132–146. Springer, 2010.
[3] Bouajjani, A., Esparza, J., and Touili, T. A Generic Approach to the Static Analysis of Concur- rent Programs with Procedures. International Journal of Foundations of Computer Science, 14(4):551–582, 2003.
[4] Cousot, P. and Cousot, R. Semantic analysis of communicating sequential processes. In Seventh International Colloquium on Automata, Languages and Programming, vol. 85 of Lecture Notes in Computer Science, p. 119–133. Springer, 1980.
[5] Cridlig, R. Implementing a Static Analyzer of Concurrent Programs: Problems and Perspectives. In Analysis and Verification of Multiple-Agent Languages, selected papers from the 5th LOMAPS workshop, vol. 1192, p. 244–259. Springer, 1997.
[6] Dijkstra, E. W. Cooperating sequential processes. Technical report, Technological University, Eindhoven, The Netherlands, 1965. Reprinted in Programming Languages: NATO Advanced Study Institute, p.43–112. Academic Press, 1968.
[7] Fajstrup, L., Goubault, É., and Raussen, M. Detecting Deadlocks in Concurrent Systems. In CONCUR’98 Concurrency Theory, vol. 1466 of Lecture Notes in Computer Science, pages 332–347. Springer, 1998.
[8] Floyd, R. W. Assigning meanings to programs. In Mathematical Aspects of Computer Science, vol.19 of Proceedings of Symposia in Applied Mathematics, p.19-32. AMS, 1967.