159 lines
No EOL
3.5 KiB
Markdown
159 lines
No EOL
3.5 KiB
Markdown
Semaphores are hard to use in practice because quite low level Monitors provide an easier definition of concurrent objects at the level of Prog. Lang.
|
|
|
|
It guarantees mutual exclusion.
|
|
|
|
Inter-process synchronization is done through *conditions*, which are objects that provide the following operations:
|
|
- ***wait*:** the invoking process suspends, enters into the condition's queue, and releases the mutex on the monitor
|
|
- ***signal*:** if no process is in the condition's queue, the nothing happens. Otherwise
|
|
- reactivates the first suspended process, suspends the signaling process that however has a priority to re-enter the monitor (*Hoare semantics*)
|
|
- completes its task and the first process in the condition's queue has the priority to enter the monitor (after that the signaling one terminates or suspends) (*Mesa semantics*).
|
|
|
|
#### A very typical use: Rendez-vous
|
|
A soon as a process arrives at a barrier it needs to suspend and wait for every other process to reach the barrier.
|
|
|
|
```
|
|
monitor RNDV :=
|
|
cnt ∈ {0,…,m} init at 0
|
|
condition B
|
|
operation barrier() :=
|
|
cnt++
|
|
if cnt < m then
|
|
B.wait()
|
|
else
|
|
cnt <- 0
|
|
B.signal()
|
|
return
|
|
```
|
|
The last process wakes up one of the others, then he wakes up another one etc...
|
|
Of course, `signal()` will have no effect on the last process who calls it.
|
|
|
|
#### Monitor implementation through semaphores
|
|
*Hoare semantics*
|
|
|
|
- A semaphore MUTEX init at 1 (to guarantee mutex in the monitor)
|
|
- For every condition C, a semaphore SEMC init at 0 and an integer $N_{C}$ init at 0 (to store and count the number of suspended processes on the given condition)
|
|
- A semaphore PRIO init at 0 and an integer $N_{PR}$ init at 0 (to store and count the number of processes that have performed a signal, and so have priority to re-enter the monitor)
|
|
|
|
Every monitor operation starts with `MUTEX.down()` and ends with `if NPR > 0 then PRIO.up() else MUTEX.up()`
|
|
|
|
```
|
|
C.wait() :=
|
|
NC++
|
|
if NPR > 0 then
|
|
PRIO.up()
|
|
else
|
|
MUTEX.up()
|
|
SEMC.down()
|
|
NC--
|
|
return
|
|
|
|
C.signal() :=
|
|
if NC > 0 then
|
|
NPR++
|
|
SEMC.up()
|
|
PRIO.down()
|
|
NPR--
|
|
```
|
|
p.s. The wait **always** suspends, even if there is only a process.
|
|
|
|
#### Readers/Writers problem, strong priority to Readers
|
|
```
|
|
monitor RW_READERS :=
|
|
AR, WR, AW, WW init at 0
|
|
condition CR, CW
|
|
|
|
operation begin_read() :=
|
|
WR++
|
|
if AW != 0 then
|
|
CR.wait()
|
|
CR.signal()
|
|
AR++
|
|
WR--
|
|
|
|
operation end_read() :=
|
|
AR--
|
|
if AR + WR = 0 then
|
|
CW.signal()
|
|
|
|
operation begin_write() :=
|
|
if (AR+WR != 0 or AW != 0) then
|
|
CW.wait()
|
|
AW++
|
|
|
|
operation end_write() :=
|
|
AW--
|
|
if WR > 0 then
|
|
CR.signal()
|
|
else
|
|
CW.signal()
|
|
|
|
```
|
|
|
|
#### Readers/Writers problem, strong priority to Writers
|
|
```
|
|
monitor RW_READERS :=
|
|
AR, WR, AW, WW init at 0
|
|
condition CR, CW
|
|
|
|
operation begin_read() :=
|
|
if WW + AW != 0 then
|
|
CR.wait()
|
|
CR.signal()
|
|
AR++
|
|
|
|
operation end_read() :=
|
|
AR--
|
|
if AR = 0 then
|
|
CW.signal()
|
|
|
|
operation begin_write() :=
|
|
WW++
|
|
if (AR + AW != 0) then
|
|
CW.wait()
|
|
AW++
|
|
WW--
|
|
|
|
operation end_write() :=
|
|
AW--
|
|
if WW > 0 then
|
|
CW.signal()
|
|
else
|
|
CR.signal()
|
|
```
|
|
|
|
#### Readers/Writers problem, a fair solution
|
|
- after a write, all waiting readers are enabled
|
|
- during a read, new readers must wait if writers are waiting
|
|
```
|
|
monitor RW_READERS :=
|
|
AR, WR, AW, WW init at 0
|
|
condition CR, CW
|
|
|
|
operation begin_read() :=
|
|
WR++
|
|
if WW + AW != 0 then
|
|
CR.wait()
|
|
CR.signal()
|
|
AR++
|
|
WR--
|
|
|
|
operation end_read() :=
|
|
AR--
|
|
if AR = 0 then
|
|
CW.signal()
|
|
|
|
operation begin_write() :=
|
|
WW++
|
|
if (AR + AW != 0) then
|
|
CW.wait()
|
|
AW++
|
|
WW--
|
|
|
|
operation end_write() :=
|
|
AW--
|
|
if WR > 0 then
|
|
CR.signal()
|
|
else
|
|
CW.signal()
|
|
```
|
|
This way nobody gets starved forever. |