Print indd

4.6
Implementation of Reference Machines
We have implemented all reference machines discussed in the previous sections
as well as many others in the synchronous programming language Quartz [
23
].
The complete implementations can be found in [
24
].
To test their correctness, programs like Dekkers mutual exclusion protocol
and programs derived from memory model litmus test suites have been success-
fully run on the presented reference machines.
While the introduced reference machines require unbounded buffers and true
nondeterminism to guarantee the completeness of the memory model, their
implementations in a system description language like Quartz have to specify
bounds for such structures. Clearly, since we can determine the required buffer
sizes for each finite execution, it is still possible to ensure the completeness. For
simulation purposes, we can resort to randomizing the nondeterministic choices,
and for verification or coverage checking, those have to be handled by oracle
inputs which are controlled by the underlying tools.