Lecture Notes for Concurrent Programming

24 June 2003 - Semaphores


Probably the easiest way to define axioms for put() and get() is to treat the binary semaphore s as a boolean variable and substitute for its underlying value in predicates. The get() axiom is

{ Q[ s <- false ]  and  s }  <s.get()>  { Q }

and the put() axiom is

{ Q[ s <- true ] }  s.put()  { Q }

Counting semaphores have a similar pair of axioms, except the counting semaphore s represents a numeric instead of a boolean value.

{ Q[ s <- s - 1 ]  and  s > 0 }  <s.get()>  { Q }

and the put() axiom is

{ Q[ s <- s + 1 ] }  s.put()  { Q }


This page last modified on 16 July 2003.