CIVL: The Concurrency Intermediate Verification Language

The CIVL-C Language

Under construction.

• CIVL-C Overview
  • structure of a CIVL-C program, top-level elements, translation to a model
• Types
  • discussion of types and their domains without syntax: primitive types, record types, scope type, proc type, pointer types, scope-parameterized pointer types, array types
  • domain of pointer types: variable references, array element references, record member reference
• Declarations
  • variable and procedure declarations, procedure definitions, scope declarations, type definitions, scope-parameterized declarations, first-class array type decls
  • declarations of system procedures, $pure procedures, procedure contracts
• Expressions
  • usual operations, array operations
• Statements
  • $spawn, $wait, $assume, ...

Contents

• Arrays
• Pointers
• MessagePassing
• OmnibusChanges
• LanguageSubset
• Examples

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).

• CIVLmeeting2013

Tool Development

• ModelChecker

• Coding Standards