CCSR: A Calculus for Communicating Shared Resources *

The timing behavior of a real-time system depends not only on delays due to process synchronization, but also on the availability of shared resources. Most current real-time models capture delays due to process ynchronization; however, they abstract out resource-specific details by assuming idealistic operating environments. On the other hand, scheduling and resource allocation algorithms used for real-time systems ignore the effect of process synchronization except for simple precedence relations between processes. To bridge the gap between these two disciplines, we have developed a formalism called Communicating Shared Resources, or CSR. This paper presents the priority-based process algebra called the Calculus.for Communicating Shared Resources (CCSR), which provides an equational characterization f the CSR language. The computation model of CCSR is resource-based in that multiple resources execute synchronously, while processes assigned to the same resource are interleaved according to their priorities. CCSR possesses a prioritized strong equivalence for terms based on strong bisimulation. The paper also describes a producer and consumer problem whose correct iming behavior depends on priority. 1 In t roduct ion The correctness of a real-time system depends not only on how concurrent processes interact, but also the time at which these interactions occur. In the tradition of untimed concurrency theory, however, formal models for tlme-dependent computation have treated the xecution of processes abstractly, quite isolated from their operating environments. These environments often have a profound effect on the timing behavior of real-time systems, and cannot be ignored when reasoning about them. To help bridge the gap between abstract computation models and implementation, we have developed a real-time formalism called Communicating Shared R sources, or CSR [4, 3]. CSR's *This research was supported in part by ONR. N000014-89-J-1131