Exercise 4

Operation Systems

• Describe the principal of scheduling and focus on the roundrobin-scheduler.

TLA+

• Indicate how to write n TLA+ modules that use the semaphore module to access a critical section as above. (That means – you don’t actually have to write them, although you could if you liked. You have to explain how they’re written, focusing on the critical details.)

• Write a TLA module that implements a counting semaphore which counts to 5 in terms of the binary semaphore module above.