An implementation of mutual inclusion
We consider the parallel composition of two cyclic programs. The interaction of these programs consists of a form of synchronisation sometimes referred to as 'mutual inclusion'. For a given implementation of this synchronisation by means of semaphore operations, we prove the correctness of the programs and we prove the absence of the danger of deadlock.
parallel composition of two cyclic programs
scientific article; zbMATH DE number 3970101