Report Number: CSL-TR-83-251
Institution: Stanford University, Computer Systems Laboratory
Title: GEM: a tool for concurrency specification and verification
Author: Lansky, Amy
Author: Owicki, Susan
Date: November 1983
Abstract: The GEM model of concurrent computation is presented. Each GEM computation consists of a set of partially ordered events, and represents a particular concurrent execution. Language primitives for concurrency, code segments, as well as concurrency problems may be described as logic formulae (restrictions) on the domain of possible GEM computations. An event-oriented method of program verification is also presented. GEM is unique in its ability to easily describe and reason about synchronization properties.
http://i.stanford.edu/pub/cstr/reports/csl/tr/83/251/CSL-TR-83-251.pdf