Proving Properties of Real-Time Semaphores

David Scholefield
Formal Systems Research Group
Department of Computer Science
University of York
Heslington, York, YO1 5DD

February 14, 1994

Abstract

Much work has been undertaken on investigating the use of semaphore primitives in concurrent programming languages. It has been shown that semaphores are adequate for expressing many forms of concurrency control, including the enforcement of communication protocols, and mutual exclusion protocols on shared resources. In this paper we present a formal language for real-time distributed programs which includes a semaphore primitive. This primitive is used to lock and unlock resources which are directly associated with either processors or communication channels. The semaphores are real-time, i.e. the programmer can express timing constraints about when the semaphores should lock and unlock. It is demonstrated that, using these semaphores, a number of apparently disjoint issues in real-time distributed systems theory can be unified within a single notion of resource restriction. In particular it is shown that different models of communication, control of shared access to resources (mutual exclusion), and process to processor mapping (physical placement), can all be expressed and reasoned about in a unified manner.

Keywords: formal verification, real-time systems, semaphores, limited resources, communication, concurrency, scheduling.