Java Team3 Benchmark3

ResourceLifecycle. This property is about an abstracted resource management system and captures the required lifecycle of a resource object.

Benchmark Data

The Trace Part

<< To appear shortly >>

The Property Part

See the rules for the necessary descriptions

Informal Description

In this scenario, a task performs many commands and each command requires resources to be taken to execute. This property only concerns the correct management of resource objects with respect to a task and command. A resource can be requested for a command running in a task - all the following activities are with respect to a command running in a task. The request can be denied or granted. If denied it can be requested again. If granted it must be released before it is requested again. All requests must be answered and all resources must be released before the end of the program. A resource cannot be granted or denied if not requested. A resource cannot be released if not granted. A resource cannot be requested if already granted.

The relevant events are therefore

• request(task,command,resource)
• grant(task,command,resource)
• deny(task,command,resource)
• release(task,command,resource)

Demonstration Traces

The following traces should be accepted

   request(T,C,A).deny(T,C,A).request(T,C,A).grant(T,C,A).release(T,C,A)
   request(T1,C1,A).request(T2,C,A).request(T3,C,A).grant(T1,C,A).deny(T3,C,A).deny(T2,C1,A).release(T,C1,A)
   request(T,C,A).deny(T,C,A)

The first and third traces are valid as the single task T, command C and resource A follow the prescribed lifecycle. The second trace is valid as there are three tasks T1, T2, and T3, which each individually interact with C and A in the valid way.

This following trace is invalid as the resource A is not released at the end of the trace.

   request(T,C,A).deny(T,C,A).request(T,C,A).grant(T,C,A)

The following trace is invalid for task T1 and command C as the resource A is granted without first being released - in the case of the second grant.

   request(T1,C,A).request(T2,C,A).request(T3,C,A).grant(T1,C,A).deny(T3,C,A).deny(T2,C,A). grant(T1,C,A).release(T1,C1,A)

The following trace is invalid as the resource A is denied to thread T and command C without first being requested - in the case of the second deny.

   request(T,C,A).deny(T,C,A).deny(T,C,A)

Formal Specification

The following QEA captures this property

   qea(ResourceLifecycle){
     Forall(task,command,resource)

     accept next(free){
       request(task,command,resource) -> requested 
     }
     next(requested){
       deny(task,command,resource) -> free
       grant(task,command,resource) -> granted
     }
     next(granted){
       release(task,command,resource) -> free
     }
   }

A next state indicates that events that have not been mentioned lead to an implicit failure state. Note that this property is with respect to a command and task. It does not hold for a resource individually.

A FO-LTL Specification

The following is a first-order LTL formulation of the property

  (forall t)(forall c)(forall r)(
       [ not ( grant(t,c,r) or deny(t,c,r) or release(t,c,r) ) Until request(t,c,r) ] and
       [ request(t,c,r) => next ( grant(t,c,r) or deny(t,c,r)  ) ] and
       [ grant(t,c,r) => next ( release(t,c,r)  ) ] and
       [ (deny(t,c,r) or release(t,c,r)) => next ( request(t,c,r) or end ) ]
   )

where

   end = never ( request(t,c,r) or grant(t,c,r) or deny(t,c,r) or release(t,c,r) )

Clarification Requests

This is a space where other teams can ask for clarifications and the submitting team can answer. When a team requests a clarification, the team should be mentioned in the request and the request timestamped. The team submitting the benchmark should ensure they watch this page so that they get notifications of questions.