|[3/4] (Im)proving Split Binary Semaphores|
por Damián Barsotti
It is well-known that binary semaphores can easily ensure mutual exclusion and therefore they can implement critical regions. Moreover, they can be used in a systematic way to implement conditional critical regions through the technique of the split binary semaphore (SBS). This technique provides not only the programs but also some invariants satisfied by the system which ensure the correctness of the solution. The programs so obtained are suitable to be optimised by analysing these invariants and using them to eliminate unnecessary tests.
It was implemented integrating the CVC Lite validity checker and Isabelle/Isar theorem prover to our program. The method was tested on a number of examples and the results are reported.
|< Anterior||Siguiente >|