Comparing the Reliability Provided by Tasks or Protected Objects for Implementing a Resource Allocation Service : a Case Study

We compare two possible implementations of a resource allocation service, one using a task server, the other using a protected object. Both make use of the requeue statement, the count attribute, and also the abort statement in order to satisfy requests, depending on the parameters passed in by the calling task and on the internal state of the service. Because the schema of requeue and entries has an execution semantic based on state and transition, it can be coupled easily with a proof in terms of colored Petri nets. We consider the dining philosophers problem, which is a good illustration of the need for a resource allocation service and for which deadlock- and starvation-free implementations have already been given in Ada95, though not formally proven and sometimes unfair. We give an almost forgotten solution where the dining philosophers problem is safely implemented with protected objects, whereas its implementation with a server task leads to deadlock. We provide two implementations, one of which completes a solution presented by Brosgol in Ada Europe 96 and makes it really fair. Informal proofs are given and are confirmed by Petri nets proofs. Through these examples, we show that the eggshell semantics of protected objects are basic for attaining a reliable implementation