|  | |||||||||
VERIFYING MULTRAN PROGRAMS WITH TEMPORAL LOGIC
Wanli Ma
Computer Sciences Laboratory, Research School of Information Science and Engineering
The Australian National University
Canberra, ACT 0200, Australia
E-mail: [email protected]
and
Mehmet Orgun
Department of Computing, School of MPCE
Macquarie University
Sydney, NSW 2109, Australia
ABSTRACT
A coordination style programming language, Multran, and its temporal logic semantics are proposed.
Multran uses Linda-like tuple space to coordinate concurrent transactions, which could
be written in any language as long as they satisfy their pre-conditions and post-conditions. It
has an intuitional presentation and enjoys a temporal logic semantics for program verification.
A Multran program can be executed in a parallel, sequential, or distributed manner based on
available resources, and its correctness can be reasoned about by temporal logic. In particular,
temporal logic can be used to reason about the safety and liveness properties of Multran
programs.
1. Introduction
Multran (Multiset transformation and transactions), a high-level parallel programming language based on multiset transformation and transaction programming paradigm, and its temporal logic semantics are proposed. Multiset, or bag, is a set except that it may have multiple occurrences of its elements. A transaction is a piece of self-contained programming code, procedure or function, which has the properties of ACID (Atomicity, Consistency, Isolation, and Durability) 10.
In Multran, the control part and computation part of a program are separated. A Multran program is composed by concurrent transactions as fundamental actions and a tuple space on which the actions take place. The elements of the tuple space are called tuples. An action happens whenever its execution condition is satisfied. It will consume certain tuples from the tuple space, execute its operations, and generate new tuples and inject them back into the tuple space for future processing. The computational model resembles a succession of chemical reactions, so-called chemical abstract machine 5;4, in which the elements of the tuple space are consumed and generated. The specification of the control part is called a Multran declaration or skeleton, and the computation part a transaction program.
As a language for parallel programming, Multran has a formal backgrounda for verification, for it is the only way to achieve robust programs. Temporal logics 26;15;20;24 are very useful to reason about on-going temporal properties, and are suitable for parallel and distributed situations. They are widely used in program specification and verification, even as programming languages 25. A temporal logic deductive system is thus used to provide formal semantics for Multran.
There are quite a few high-level parallel programming languages and/or paradigms. Multran is deeply rooted in Linda 13;7, GAMMA 1;2;3, and Unity 8. To summarize, (i) Multran inherits the idea of coordination and tuple space from Linda, (ii) the chemical reaction metaphor comes from GAMMA to control the process of computation, and (iii) the separation of formal verification from program presentation as in Unity will benefit both program verification and development.
aWe emphasize the background" because the formal part can be separated from the program presentation.