Exercise 2

Operation Systems

• Explain how a Semaphore works and why we need this.

TLA+

• Write a TLA+ module that specifies a (binary) semaphore. That means: data structures, operations, initial conditions, and the specification with initial and safety conditions only. (Liveness conditions are needed, but we won’t bother with those yet).

• Write TLA+ modules for two processes that use the semaphore module to

– increment x continually (x is a variable of the process);

– increment y continually (y is a variable of the process).

The increment command is the critical section for each process.