put() and get() entries.
get() -> get() -> put()
get() must follow, not precede put().
put() -> put() -> get() -> get()
The Specification of Process Synchronization by Path Expressions by R. Campbell and N. Habermann, Proceedings of an International Symposium on Operating Systems (LCNS 16), Springer-Verlag, April 1974.
path exp
, exp1
; exp1
( exp ) group and nest as they usually
do.
[ exp ]
path put() , get()
is an unsatisfactory specification for semaphores. (Why?)
path put() ; get()
is also an unsatisfactory specification for a semaphore, but less so than the previous specification (Why?)
path [ put() ] , 1 : get()
should specify a binary semaphore, but not a counting semaphore (Why?)
monitor
OneSlotBuffer
data buffer
path put ; get
void put(data d)
buffer = d
void get(data & d)
d = buffer
|
monitor
OneSlotBuffer
data buffer
cond empty = true
full = false
void put(data d)
empty.wait()
buffer = d
full.signal()
void get(data & d)
full.wait()
d = buffer
empty.signal()
|
monitor OneSlotBuffer
path put(data din) ; get(data & dout) {
dout = din
}
1 : [ exp ].
async.
path put(data din) ; get(data & dout) {
dout = din
}
to
async put(data din) & get(data & dout) {
dout = din
}
class ReadersWriters
void writerEnter() &
async Idle() { }
void writerExit()
Idle()
void readerEnter() &
async idle()
readerCount(1)
void readerEnter() &
async readerCount(int n)
readersCount(n + 1)
void readerExit() &
async readerCount(int n)
if n = 1
Idle()
else
readersCount(n - 1)
ReadersWriters
idle()
This page last modified on 14 August 2003.