L. Chen and M. Mizuno (USA)
Concurrency, Global invariant, Synchronization, Thread pool model
Andrews'global invariant approach is a formal develop ment process for concurrent programs. In this approach, the safety properties for synchronization are specified in terms of global invariants. The global invariants are me chanically translated to synchronization code via so-called coarse-grained solutions. This paper presents a translation algorithm from coarse-grained solutions to fine-grained synchronization code for a thread-pool model. In our trans lation, when an execution needs to be blocked, synchro nization code releases and returns the executing thread to the thread pool, rather than blocking it, so that the thread can execute another job. Using our translation, deadlock due to the lack of threads never occurs.
Important Links:
Go Back
