In: Proc. Asia-Pacific Software Engineering Conf. and Int. Computer Science Conf., 2-5 December 1997, Hong Kong, pages 238-248. 1997. ISBN 0-8186-8271-X, IEEE CS No. PR08271, IEEE Catalog No. 97TB100207.
Abstract: 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. The aim of the presented approach 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 that has 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. This is why the paradigm of dining philosophers was chosen. The paper contains three programmed solutions and proofs of absence of deadlocks and of starvation.
Keywords: ADA-95, Petri nets, preference control.