Softwar Design Laboratory at  MichiganTech

Towards the Model Checking of the Partitioned Global Address Space (PGAS) Applications

Objectives

The objective of this project is to enable and evaluate the model checking of the inter-thread synchronization mechanisms, called the synchronization skeletons, of Unified Parallel C (UPC) programs using the SPIN model checker.

UPC is an extension of the C Programming language that provides Single Program Multiple Data (SPMD) parallel execution in the PGAS memory model. Specifically, we anticipate the following technical contributions for this project:

· To create a method for extracting synchronization skeletons of UPC programs;

· To develop a systematic approach for enabling programmers to specify the desired behaviors/properties of their UPC programs, such as mutual exclusion and progress properties, appropriate for SPIN;

· To develop a set of semantics-preserving transformation rules for translating the extracted synchronization skeletons of UPC programs to Promela models depending on the property of interest, and

· To develop a set of visualization rules for representing behavioral errors reported by SPIN in UPC programs.

This project will also experimentally determine whether model checking the Promela models of UPC programs can reveal errors in programs claimed to be error-free.