Busy Waiting - Further Study
The Mutual Exclusion Problem
Our presentation of busy waiting is based on material found in
many places, but most importantly in Ben-Ari's books
[ B-A82 ,
B-A90 ].
If you would rather hear about the MEP from a better source than I
then investigate his books.
Another reommended source for the MEP is
[ An91 ].
Proofs for Correctness Properties
Dekker's Algorithm cannot be accepted as a `correct' solution to the MEP
until it can be proven to have both the safety mutual
exclusion proerty and that it cannot livelock.
As no amount of testing can prove such correctness we have
to construct a formal proof.
Ben-Ari [ B-A90 ]
proves the correctness properties of each attempted solution
using temporal logic.
For any imperative concurrent language such as Java
temporal logic is a major tool in proving the correctness of
concurrent programs.
Anyone with time to spare would profit from Ben-Ari's proof
theoretic presentation of the MEP.
It is truly unfortunate that we do not have time in CS237
to study the MEP material with more emphasis on proving correctness.
Learning Java
The challenge here is to understand how multiple threads are set up in Java.
Most Java texts will have a chapter or section on multi-threading, for example,
Java Gently [ Bi98 ].