Menu Content/Inhalt
Home arrow Seminarios arrow [3/4] (Im)proving Split Binary Semaphores
[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.
This work presents a mechanical method to perform these optimisations. The method use the backward propagation technique over a guarded transition system that models the behavior of the programs generated by the SBS technique.

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 >
Content Management System: Joomla!
Template based on an original designed by