= CIVL: The Concurrency Intermediate Verification Language =

Contents
* [wiki:Pointers]
* [wiki:MessagePassing]


== Thoughts about the CIVL-C language ==

* Would it be nice to add an atomic statement to CIVL?  Semantics: there is a single global lock, initially available.   The guard of every transition in the model is effectively modified so that it is enabled only if the lock is free or owned by the process executing the transition.  Entering an atomic region obtains the lock, exiting releases it.  Hence no other process can run while one is inside an atomic region.  How will this complicate reasoning about CIVL models?
* It might be nice to introduce some convenience constructs that are syntactic sugar for commonly occurring patterns.  For example, something like "$proc p = $run stmt" which is short for declaring a temporary procedure with body stmt and spawning that procedure.  Also, something like "$waitall($proc procs[], int numProcs);" (that one can be defined as a library function).