CIVL

Overview

CIVL consists of a programming language, CIVL-C, a model checker, and compilers that translate programs written in common parallel languages (such as MPI and Cuda) to CIVL-C. See the main project site for more details.

In collaboration with the Verified Software Laboratory, we are

  • developing models of Cuda programs in CIVL
  • writing the formal semantics for CIVL-C

This work is supported by NSF award CCF 1346756.

Cuda Models

Coming soon ...

Formal Semantics

CIVL-C is based on a subset of C11, with additional features for expressing concurrency, assertions and function contracts, and modeling artifacts (see the manual).

To balance precision, clarity, and ease of understanding, we have chosen to use (structural) operational semantics to describe how expressions and statements in CIVL-C are interpreted by the model checker. The abstract machine consists of a list of processes and a dynamic scope tree for resolving variable references and memory accesses. Each process maintains a "stack" and the program it is currently executing.

We have successfully modeled function calls, variable resolution, $spawn, and $wait. Each of these require traversing and/or updating the dynamic scope tree.

The semantics is currently given in PLT-Redex, a domain specific language for describing the structural operational semantics for programming languages (the resulting specification is executable). To execute our specification for CIVL-C,

  1. Install Racket. The distribution should include the DrRacket IDE and the PLT-Redex module.
  2. Download and unpack our spec: civl-c-spec.tar.gz.
  3. civl-0.rkt contains the main part of the specification for the abstract machine and basic expressions. civl-1.rkt contains CIVL-C specific statements. You have a couple of choices:
    • To run a simple one-process evaluator, open and run civl-fe.rkt.
    • To run the tests in either civl-0.rkt or civl-1.rkt, open either one in DrRacket and click Run. (You can also run the tests e.g. using raco test civl-0.rkt on the command line.)

Fenceless Floating Point Algorithms

We investigated the performance and accuracy of parallel iterative floating point algorithms when fences and other forms of synchronization were removed.

The project report is available here, and the source code used in the project is here.