SyncGen Architecture



In our approach (refer to the figure above), the developer builds core functional code without implementing the synchronization policy. For example, in a readers-writers system, code to access a shared buffer would be written. The developer delimits particular code regions that will be synchronized. In a readers-writers system, one would mark the regions that access shared data as a reader and those that access the data as a writer. A synchronization policy that controls the scheduling of threads that attempt to execute in those regions is specified in a language of global invariant patterns. This synchronization specificiation is compiled to a predicate representing an invariant that must hold on the region. These invariants can then be used to generate implementations of the synchronization policy in Java, for example, that are then integrated with the core functional code to produce a complete concurrent application.

This process guarantees that the safety properties described by the invariant are correctly implemented by construction. To guard against errors in the synthesis process we can encode specifications of the intended synchronization properties into the generated code and apply model checking to verify that they hold. This kind of checkable redundancy yields a high degree of confidence in the correctness of our synthesis approach. This confidence does not, however, extend to additional correctness properties, e.g., liveness properties, that one might wish to check. To address this, we have adapted the Bandera toolset to extract models that are a hybrid of synchronization specifications and core functional code. The resulting models encode program synchronization very efficiently, yielding dramatic state-space reductions that promise to increase the size and complexity of systems for which model checking is tractable.

Our approach builds off and extends the global invariant approached advocated by Andrews. Our main extensions have been to identify recurring patterns of global invariant specification, to revise the methodology for developing implementations of those specifications, and to provide automated tool support for the synthesis of implementations. We believe the result is a framework for developing correct efficient synchronization code that is:

  • Powerful -- using the pattern system, complicated structures can be described clearly and succinctly at a very high level;
  • Expressive -- we have used the pattern system to specify solutions for a wide variety of exercises from three well-known concurrency texts\cite {Andrews:91,Andrews:00,Ha98};
  • Automatic -- this is push-button approach where code with very intricate semantics is automatically generated from high-level specifications;
  • General -- the approach is language independent and supports multiple languages and synchronization primitives;
  • Formal -- our aspect specification language has a rigorous semantic foundation which enables code generation techniques that use decision procedures for a quantifier-free fragment of first-order arithmetic and yields a high degree of confidence in the generated solutions; and
  • Verifiable -- the structure of the generated code and associated artifacts is designed so that crucial correctness requirements can be checked automatically using existing software model-checking technology.