Java Team3 Benchmark1

PublisherSubscriber. The setting is that of publisher and subscriber nodes where publisher nodes broadcast messages and subscriber nodes acknowledge received messages. The property makes use of complex quantifier alternation.

Categories: Communication

Benchmark Data

The Trace Part

<< Details about Java program to follow >>

The Property Part

Informal Description

The setting is that of publisher and subscriber nodes where publisher nodes broadcast messages and subscriber nodes acknowledge received messages. We observe two events: send(publisher,msg) indicates that the publisher broadcast the msg, and ack(subscriber,msg) indicates that the subscriber received the message. There are three kinds of objects that will be observed: publishers, subscribers and messages. For quantification purposes the set of relevant objects can be taken as those found in the trace as identified by the previous events i.e. if send(A,m) is seen then A is a relevant publisher and m is a relevant message.

The property is that for every publisher, there exists a subscriber that acknowledges every message sent by that publisher. In other words, every publisher has a subscriber that reads all of its messages. The set of messages a publisher sends is defined by the send event. Note that the acknowledgement must come after the sending.

Publishers, subscribers and messages can be identified as references i.e. using == in Java.

It is not assumed that two publishers cannot send the same message, this allows for a situation where a publisher repeats another publishers message. Acknowledgements without previous send events are allowed. If a publisher resends the same message then a new acknowledgement is required.

Demonstration Traces

The following traces should be accepted

   send(P,m1).send(P,m2).ack(S,m2).ack(S,m1)
   send(P,m1).send(Q,m1).ack(S,m1)
   send(P,m1).send(Q,m2).ack(S,m1).ack(T,m2)

The first shows that the messages do not need to be acknowledged in the order they were sent. The second shows that a single subscriber could acknowledge all messages from multiple publishers. The third is the more common case where separate subscribers are acknowledging messages from different publishers.

The following traces should be rejected

   send(P,m1).ack(S,m1).send(P,m2).ack(T,m1)
   send(P,m1).send(P,m2).ack(S,m2).sent(Q,m2).ack(S,m1)
   send(P,m1).ack(S,m1).send(P,m1).ack(T,m1)

The first is bad because nobody acknowledges the m2 message from P. The second is bad as nobody acknowledges the m2 message from Q; the earlier acknowledgement does not count. The third is bad because the message m1 was sent twice by P but acknowledged by different subscribers. Below we show one way to fix each of the above bad traces

   send(P,m1).ack(S,m1).send(P,m2).ack(T,m1).ack(S,m2)
   send(P,m1).send(P,m2).ack(S,m2).sent(Q,m2).ack(S,m1).ack(T,m2)
   send(P,m1).ack(S,m1).send(P,m1).ack(T,m1).ack(S,m1)

Formal Specification

This property can be captured by the following QEA

   qea(PublisherSubscriber){
       Forall(publisher) Exists(subscriber) Forall (msg)
   
       accept skip(NotSent){ 
           send(publisher,msg) -> Sent 
       }
       skip(Sent){ 
           ack(subscriber,msg) -> NotSent
           send(publisher,msg) -> Failure
       }
   }

The transition to failure in the Sent state is required as if the publisher sends the message again without it being acknowledged then that subscriber has not acknowledge the previous copy of that message.

The skip modifier indicates that all other events are skipped (the state is preserved). This allows arbitrary acknowledge events in the NotSent state. The Sent state is not given the accept modifier as the trace ending in this state indicates that the subscriber did not acknowledge (every copy of) that message.

A FO-LTL Specification

In first-order LTL one could write

   (forall publisher)(exists subscriber)
           (forall msg)(always send(publisher,msg) => (not send(publisher,msg) Until ack(subscriber,msg)))

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.