View source for 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/bench2

The program consists of 6 Java files. The main file Run.java (deterministically) creates a number of social network sites and nice people and makes a certain number of steps. Then an annoying person is added and more steps are made which contain the bad behaviour of this annoying person.

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 bench2

and to execute the program run

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

The program will produce 5,050,000 events, there is a single kind of event for this property, the send event. 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.