Petri nets based proofs of Ada 95 solution for preference control

This paper presents correctness proofs of Ada 95 preference control solution for the dining philosophers paradigm. Preference control is the ability to satisfy a request depending on the parameters passed in by the calling task and often also on the internal state of the server. In Ada 95, this schema is implemented with protected objects, entry families and requeue statements within the protected object. Our aim is to show that the preference control can be described in terms of states and transitions, similar to reactive automaton descriptions. This description, which can be done in terms of colored Petri nets, can lead jointly to validate the chosen implementation and to program it with protected objects and requeue statements of Ada 95. The paper is issued from an examination exercise for our students that have followed a course on Programming and Validation of Concurrent Applications and is presented in form of progressive steps for which the students were expected to give answer. The paper contains three programmed solutions and proofs of absence of deadlock and of starvation