Publication View

On proof rules for monitors (1982)

Abstract
An inadequacy is pointed out in the original proof rules for monitors and in later extended rules. This inadequacy gives rise to an anomaly in proving the invariant for a monitor simulating a counting semaphore. New proof rules are proposed and used to give a sound proof of the invariant.

Publication details
Download http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.85.1693
Source http://web.cecs.pdx.edu/~black/publications/OnProofRules.pdf
Contributors CiteSeerX
Repository CiteSeerX - Scientific Literature Digital Library and Search Engine (United States)
Keywords Key Words and Phrases, concurrency, monitor, operating system
Type text
Language English
Relation 10.1.1.91.3720, 10.1.1.49.1927, 10.1.1.103.9395, 10.1.1.131.7439