||Systematic Removal of Nondeterminism for Code Generation in I/O Automata
||Joshua A. Tauber, Michael J. Tsai, Nancy Lynch
|LCS Document Number:
||Theory of Computation
|The Input/Output (I/O) automaton model developed by Lynch and Tuttle models components in asynchronous concurrent
systems as labeled transition systems. IOA is a precise language for describing I/O automata and for stating their properties. A toolset is being
developed for IOA to support distributed software design and implementation. One of the tools consists of a user
assisted code generator from
IOA into an imperative programming language such as C or Java.
One aspect that distinguishes IOA programs from programs written in
imperative languages is the presence of nondeterminism which comes
in the form of explicit nondeterministic statements and implicit scheduling choices made during execution. Code generation therefore consists
partially of systematically removing all forms of nondeterminism.
In this paper, we describe our approach and design for code generation.
We focus on the issue of removing implicit nondeterminism and specify a transformation on IOA programs that makes all nondeterminism
explicit. The programmer can then replace all explicit nondeterminism
with deterministic statements prior to code generation. We also describe
this transformation at a semantic level i.e., at the level of the I/O automaton mathematical model. We show that the transformation defined
at the IOA level conforms to the one at the semantic level.
|To obtain this publication:
To purchase a printed copy of this publication please contact