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

See marq/java/bench1

The program consists of 6 Java files. The main file Run.java (deterministically) creates a number of nodes that broadcast to a single channel and subscribe to multiple channels. A certain number of steps are taken where a node produces a message and broadcasts it. Some kinds of messages are forwarded by nodes.

An AspectJ file is provided that prints the events and can be used for monitoring.

To compile the program with instrumentation run

  java -cp "lib/*" org.aspectj.tools.ajc.Main -source 1.7 -d bin -sourceroots bench1

and to execute the program run

  java -cp "lib/*:bin" bench1.Run

The program will produce 13,972 events. With 1,380 send events and 12,592 ack events. The program violates the property.

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.

• The trace part section seems to be swapped with Benchmark1 and Benchmark2. Furthermore, I get the following different number of events through multiple runs. For a fair competition, I suppose, it would be better, to get this more deterministic. -- Malte, 2016-07-07T15
  • • broadcast: 1380
    • acknowledge: 13464
    • events: 14844
  • • broadcast: 1380
    • acknowledge: 15315
    • events: 16695
  • • broadcast: 1380
    • acknowledge: 14716
    • events: 16096

• I've swapped the trace parts for Benchmark1 and Benchmark2. The non-determinism worries me. I checked quite carefully that the benchmark was deterministic and it still appears deterministic on my machine. If it is non-deterministic then the status of the benchmark might change! I am not sure where this is coming from, any thoughts would be useful.