Skip to content

Commit

Permalink
Merge pull request #2 from RoryMalcolm/multi_party_session_types
Browse files Browse the repository at this point in the history
Multi party session types
  • Loading branch information
rorymalcolm committed Jul 28, 2018
2 parents 6aad4d7 + 7164509 commit 93218bd
Show file tree
Hide file tree
Showing 30 changed files with 652 additions and 150 deletions.
8 changes: 5 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,19 +13,21 @@ Protocol protocol = protocolBuilder
.node()
.payload(null)
.connection()
.actor("0")
.fromActor("0")
.toActor("1")
.to("1")
.node()
.payload(TestClass.class)
.connection()
.actor("0")
.fromActor("0")
.toActor("1")
.to("1")
.build();
ProtocolMonitor monitor = new ProtocolMonitor(protocol);
monitor.addActor(new QueueActor());
monitor.addActor(new QueueActor());

monitor.send("0", "1", new TestClass("Hello!"));
monitor.send("1", "0", new TestClass("Hello!"));
```

## Examples
Expand Down
Binary file modified documentation/Thesis/thesis.pdf
Binary file not shown.
2 changes: 1 addition & 1 deletion documentation/Thesis/thesis.tex
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@

One considered approach was a ``chained types'' implementation, this would have provided a set of types in Java to construct a larger session. An example of this would have been a ``decision'' type, which took two type parameters, with the signature \texttt{Decision<S,T>} where supplying S or T would have forced the protocol to take a different path depending on the input. However as displayed in a paper which uses this approach earlier\cite{jespersen2015session}, any reasonably complicated protocol implementation using this appproach has a unruly type signature which is hard to parse and harder to create. As the aim of the project is to create an easily usable ``plug and play'' library to enhance and improve safety and security in Java programs, it is important to avoid obnubilating protocol structure from a reader.


During the development process, the settled upon protocol representation strategy resembled an implementation of Finite State Machines. Finite state machines are a form of directed graph, a collection of nodes connected to each other with edges, representing ``valid'' states a system can have and what legal moves can be made between these states depending on certain conditions. In the protocol graph, a ``state'' is a node which contains a type, these nodes are then connected with edges which have a guard specifying which actor can traverse along them. An example of a graph which allows to actors to say hello to each other before terminating the communication would have three nodes. The first node, would have a \texttt{null} payload and an edge containing a reference to actor 0 to another node which contained \texttt{Hello.class} finally this node would have an edge containing a reference to actor 1 to a final node that also had the payload \texttt{Hello.class}.
\subsection{Graph Traversal}
\subsection{Domain Specific Language}
Users having the ability to express the structure of complex protocols easily is key to the adoption of the library by a wider user-base. It is paramount that this is made as simple as it possibly can, to improve both usability when creating the protocol structure and comprehension when checking it at a later date. As expressed in the literature review, one such standard approach is the Scribble\cite{honda2011scribbling} domain description language, where users create protocols and then use tools to compile the contents to an implementation usable with their language of choice. In a library sense, however, this is imperfect, it requires an extra layer of knowledge from users outside of the normal language paradigm, it increases the learning curve, potentially putting off new users, and requires some form of parsers and compilation process which could prove difficult to implement in the time constraints of the project.
Expand Down
20 changes: 10 additions & 10 deletions src/main/java/com/dynosesh/ProtocolMonitor.java
Original file line number Diff line number Diff line change
Expand Up @@ -34,20 +34,20 @@ public ProtocolMonitor(Protocol protocol) {
}

/**
* Adds and actor to the protocol's dictionary.
* Adds and toActor to the protocol's dictionary.
*
* @param actor The actor reference
* @param actor The toActor reference
*/
public void addActor(Actor actor) {
this.actorMap.put(String.valueOf(actorCount), actor);
actorCount++;
}

/**
* Returns the actor with the corresponding key.
* Returns the toActor with the corresponding key.
*
* @param key The key for searching the map with
* @return The actor object
* @return The toActor object
*/
public Actor getActor(String key) {
return this.actorMap.get(key);
Expand All @@ -56,17 +56,17 @@ public Actor getActor(String key) {
/**
* Sends a message, and ensures it complies to the protocol.
*
* @param senderAddress The address of the actor sending the request
* @param receiverAddress The address of the actor to send the message to
* @param payload The message to send to an actor
* @param receiverAddress The address of the toActor to send the message to
* @param senderAddress The address of the toActor sending the request
* @param payload The message to send to an toActor
* @throws InvalidSessionException Thrown when there is a session type error
*/
public void send(String senderAddress,
String receiverAddress, Sendable payload) throws InvalidSessionException {
public void send(String receiverAddress, String senderAddress,
Sendable payload) throws InvalidSessionException {
if (this.actorMap.size() == 0) {
throw new IllegalArgumentException("The protocol does not currently contain actors");
}
if (this.protocol.checkStatusAndProgress(senderAddress, payload)) {
if (this.protocol.checkStatusAndProgress(receiverAddress, senderAddress, payload)) {
try {
this.actorMap.get(receiverAddress).sendTask(payload);
} catch (NullPointerException e) {
Expand Down
8 changes: 4 additions & 4 deletions src/main/java/com/dynosesh/actor/Actor.java
Original file line number Diff line number Diff line change
Expand Up @@ -6,16 +6,16 @@
public interface Actor {

/**
* Sends a task to the actor specified
* Sends a task to the toActor specified
*
* @param sendable The task to send to the actor
* @param sendable The task to send to the toActor
*/
void sendTask(Sendable sendable);

/**
* Receives a task from the actor specified
* Receives a task from the toActor specified
*
* @return The task from the actor
* @return The task from the toActor
*/
Sendable receiveTask() throws InvalidSessionException;
}
4 changes: 2 additions & 2 deletions src/main/java/com/dynosesh/actor/QueueActor.java
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ public QueueActor() {
}

/**
* Adds a task to the actor's task queue
* Adds a task to the toActor's task queue
*
* @param sendable The task for adding to the queue
*/
Expand All @@ -33,7 +33,7 @@ public void sendTask(Sendable sendable) {
}

/**
* Gets the task on the top of the actor's task queue
* Gets the task on the top of the toActor's task queue
*
* @return The task at the top of the queue
*/
Expand Down
80 changes: 48 additions & 32 deletions src/main/java/com/dynosesh/example/http/Runner.java
Original file line number Diff line number Diff line change
Expand Up @@ -50,21 +50,25 @@ private static void firstSectionOfTransmission(ProtocolBuilder protocolBuilder)
.node()
.payload(null)
.connection()
.actor(CLIENT_ADDRESS)
.to("1")
.fromActor(CLIENT_ADDRESS)
.toActor(SERVER_ADDRESS)
.to("1")
.node()
.payload(Hello.class)
.connection()
.actor(SERVER_ADDRESS)
.to("2")
.fromActor(SERVER_ADDRESS)
.toActor(CLIENT_ADDRESS)
.to("2")
.node()
.payload(Hello.class)
.connection()
.actor(SERVER_ADDRESS)
.to("3")
.fromActor(SERVER_ADDRESS)
.toActor(CLIENT_ADDRESS)
.to("3")
.connection()
.actor(SERVER_ADDRESS)
.to("5");
.fromActor(SERVER_ADDRESS)
.toActor(CLIENT_ADDRESS)
.to("5");
}

private static void secondSectionOfTransmission(ProtocolBuilder protocolBuilder) {
Expand All @@ -74,13 +78,15 @@ private static void secondSectionOfTransmission(ProtocolBuilder protocolBuilder)
.node()
.payload(HelloDone.class)
.connection()
.actor(CLIENT_ADDRESS)
.to("4")
.fromActor(CLIENT_ADDRESS)
.toActor(SERVER_ADDRESS)
.to("4")
.node()
.payload(ClientKeyExchange.class)
.connection()
.actor(CLIENT_ADDRESS)
.to("12");
.fromActor(CLIENT_ADDRESS)
.toActor(SERVER_ADDRESS)
.to("12");
}

private static void thirdSectionOfTransmission(ProtocolBuilder protocolBuilder) {
Expand All @@ -90,38 +96,45 @@ private static void thirdSectionOfTransmission(ProtocolBuilder protocolBuilder)
.node()
.payload(Certificate.class)
.connection()
.actor(SERVER_ADDRESS)
.to("6")
.fromActor(SERVER_ADDRESS)
.toActor(CLIENT_ADDRESS)
.to("6")
.node()
.payload(ServerKeyExchange.class)
.connection()
.actor(SERVER_ADDRESS)
.to("7")
.fromActor(SERVER_ADDRESS)
.toActor(CLIENT_ADDRESS)
.to("7")
.node()
.payload(CertificateRequest.class)
.connection()
.actor(SERVER_ADDRESS)
.to("8")
.fromActor(SERVER_ADDRESS)
.toActor(CLIENT_ADDRESS)
.to("8")
.node()
.payload(HelloDone.class)
.connection()
.actor(CLIENT_ADDRESS)
.to("9")
.fromActor(CLIENT_ADDRESS)
.toActor(SERVER_ADDRESS)
.to("9")
.node()
.payload(Certificate.class)
.connection()
.actor(CLIENT_ADDRESS)
.to("10")
.fromActor(CLIENT_ADDRESS)
.toActor(SERVER_ADDRESS)
.to("10")
.node()
.payload(ClientKeyExchange.class)
.connection()
.actor(CLIENT_ADDRESS)
.to("11")
.fromActor(CLIENT_ADDRESS)
.toActor(SERVER_ADDRESS)
.to("11")
.node()
.payload(CertificateVerify.class)
.connection()
.actor(CLIENT_ADDRESS)
.to("12");
.fromActor(CLIENT_ADDRESS)
.toActor(SERVER_ADDRESS)
.to("12");
}

private static void finalSectionOfTransmission(ProtocolBuilder protocolBuilder) {
Expand All @@ -130,18 +143,21 @@ private static void finalSectionOfTransmission(ProtocolBuilder protocolBuilder)
.node()
.payload(ChangeCipherSpec.class)
.connection()
.actor(CLIENT_ADDRESS)
.to("13")
.fromActor(CLIENT_ADDRESS)
.toActor(SERVER_ADDRESS)
.to("13")
.node()
.payload(Finished.class)
.connection()
.actor(SERVER_ADDRESS)
.to("14")
.fromActor(SERVER_ADDRESS)
.toActor(CLIENT_ADDRESS)
.to("14")
.node()
.payload(ChangeCipherSpec.class)
.connection()
.actor(SERVER_ADDRESS)
.to("15")
.fromActor(SERVER_ADDRESS)
.toActor(CLIENT_ADDRESS)
.to("15")
.node()
.payload(Finished.class);
}
Expand Down
2 changes: 1 addition & 1 deletion src/main/java/com/dynosesh/example/http/SocketActor.java
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ public Sendable receiveTask() throws InvalidSessionException {
this.objectInputStream = new ObjectInputStream(inputStream);
}
Sendable sendable = (Sendable) this.objectInputStream.readObject();
protocolMonitor.send(this.address, sendable.getTarget(), sendable);
protocolMonitor.send(sendable.getTarget(), this.address, sendable);
return sendable;
} catch (IOException | ClassNotFoundException e) {
e.printStackTrace();
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
package com.dynosesh.example.multiparty.bookstore;

import com.dynosesh.Sendable;
import com.dynosesh.example.multiparty.bookstore.types.Okay;
import com.dynosesh.example.multiparty.bookstore.types.SendableDateTime;
import com.dynosesh.example.multiparty.bookstore.types.SendableInteger;
import java.io.IOException;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.net.Socket;
import java.util.Date;

public class BookStore implements Runnable {

private int port;

public BookStore(int port) {
this.port = port;
}

@Override
public void run() {
try {
Socket socket = new Socket("localhost", port);
ObjectOutputStream objectOutputStream = new ObjectOutputStream(socket.getOutputStream());
objectOutputStream.flush();
ObjectInputStream objectInputStream = new ObjectInputStream(socket.getInputStream());
streamsInitialised(objectOutputStream, objectInputStream);
} catch (IOException e) {
e.printStackTrace();
} catch (ClassNotFoundException e) {
System.out.println("Protocol was violated on the BookStore!");
e.printStackTrace();
}
}

private void streamsInitialised(ObjectOutputStream objectOutputStream,
ObjectInputStream objectInputStream) throws IOException, ClassNotFoundException {
Sendable inputTitle = (Sendable) objectInputStream.readObject();
System.out.println("BookStore: received " + inputTitle.getPayload());
objectOutputStream.writeObject(new SendableInteger(10, "1"));
objectOutputStream.writeObject(new SendableInteger(10, "2"));
objectOutputStream.writeObject(new Okay(true, "1"));
Sendable inputOkay = (Sendable) objectInputStream.readObject();
Sendable inputAddress = (Sendable) objectInputStream.readObject();
System.out.println("BookStore: received address " + inputAddress.getPayload());
objectOutputStream.writeObject(new SendableDateTime(new Date(), "2"));
Sendable inputQuit = (Sendable) objectInputStream.readObject();
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
package com.dynosesh.example.multiparty.bookstore;

import com.dynosesh.Sendable;
import com.dynosesh.example.multiparty.bookstore.types.SendableInteger;
import com.dynosesh.example.multiparty.bookstore.types.SendableString;
import java.io.IOException;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.net.Socket;

public class BuyerOne implements Runnable {

private int port;

public BuyerOne(int port) {
this.port = port;
}

@Override
public void run() {
try {
Socket socket = new Socket("localhost", port);
ObjectOutputStream objectOutputStream = new ObjectOutputStream(socket.getOutputStream());
objectOutputStream.flush();
ObjectInputStream objectInputStream = new ObjectInputStream(socket.getInputStream());
streamsInitialised(objectOutputStream, objectInputStream);
} catch (IOException e) {
e.printStackTrace();
} catch (ClassNotFoundException e) {
System.out.println("Protocol was violated on BuyerOne!");
e.printStackTrace();
}

}

private void streamsInitialised(ObjectOutputStream objectOutputStream,
ObjectInputStream objectInputStream) throws IOException, ClassNotFoundException {
objectOutputStream.writeObject(new SendableString("The New Old World by Perry Anderson",
"0"));
Sendable quote = (Sendable) objectInputStream.readObject();
System.out.println(" BuyerOne: quote is " + quote.getPayload());
Sendable okay = (Sendable) objectInputStream.readObject();
System.out.println(" BuyerOne: received Okay");
Integer returnValue = (Integer) quote.getPayload();
objectOutputStream.writeObject(new SendableInteger(returnValue / 2, "2"));
}

}

0 comments on commit 93218bd

Please sign in to comment.