Apims
From thelas.dk
apims is an interpretor for the Asynchronous PI-calculus with Multiparty session types and Symmetric sum types. The key features of this interpretor are the symmetric sum types and that the interpretor can display GUI's for each process in each session, to enable user agreement and input. This interpretor has been developed as a proof of concept implementation of some of the theoretical work I have done in my PhD project. Since this is a proof of concept implementation, the users should be prepared to find bugs, but currently there are no known bugs.
apims is a c++ library, but contains sample programs to typecheck and evaluate code. The installation instructions includes an example of how to evaluate code.
Contents |
Requirements
- DynParser is used to parse the given programs.
- SDL and in particular the network library libsdl-net is used to start a webserver that allows user-interaction with the running processes.
Versions / Download
- apims-1.5.0 Proof of Concept release
Installation Instructions
The usual installation procedure is as follows
tar -xvzf apims-1.5.0.tgz cd apims-1.5.0 make config make build sudo make install cd programs make config make build sudo make install cd apims_code apims -f example.mps
Now the installation procedure will be explained in more detail.
Before installing the apims library, make sure you have installed the requirements.
When the necessary dependencies have been installed, apims is downloaded using the above link.
The rest of the installation is done using a shell or terminal.
To unpack the downloaded file, go to the directory containing the downloaded file and execute tar -xvzf apims-1.5.0.tgz.
Then enter the created folder by executing cd apims-1.5.0.
Now it is time to create a Makefile from the Makefile.in by typing make config.
The apims library can now be compiled by typing make build.
Finally install the library by executing make install as root.
If no errors were encountered the project is now installed, and you can start using the library.
To install the apims interpretor, enter the programs folder by typing cd programs.
Then build the interpretor in the same way as the library, by executing make config,
make build and finally make install as root.
Now the interpretor is installed, and it can be used to evaluate programs.
An array of sample programs are in the apims_code folder. Enter this folder by typing cd apims_code.
Now evaluate the example.mps program by typing apims -f example.mps. This will evaluate the sampel program, writing each step in the evaluation to the console.
Tutorial
Apims is build on the pi-calculus with multiparty session types. This is fundamentally different from most programming languages, and therefore apims may seem like a strange language at first. This approach however means that apims gains from the extensive research invested in the pi-calculus, offering the programmer and user some unique guarantees.
The basic concepts in apims are processes, channels, messages and sessions. Basically a process is a program. It can communicate with other processes by sending messages over channels. Now we just need to understand what sessions are. A session is a collection of channels that follow a specified network-protocol. In stead of using many pages to explain these concepts in detail as it is done on wikipedia, this section will in stead give a number of examples to develop the intuitive understanding of the language.
Starting a session
(nu a: Gend) ( link(2,a,s,1); end | link(2,a,s,2); end )
The above example is actually two processes.
The first process link(2,a,s,1);end uses channel a to create the session s with two participants where the process is participant nr. 1, and then the process ends.
The second process link(2,a,s,2);end uses channel a to create the session s with two participants where the process is participant nr. 2, and then the process ends.
The (nu a: Gend) specifies that the channel a can be used to create sessions on, and Gend is the protocol of the created sessions. Gend is the name of the completed protocol, and this means that no messages can (or must) be sent on the sessions created on a.
Sending a message
(nu a: 1=>2:1<Int>;Gend) ( link(2,a,s,1); s[1]<<5; end | link(2,a,s,2); s[1]>>x; end )
The above example is similar to the first example, and consists of two processes.
The first process link(2,a,s,1);s[1]<<5;end creates the session s on channel a, and continues as participant 1 out of 2. Then the process sends the integer 5 on channel 1 in session s, and then the process ends.
The second process link(2,a,s,2);s[1]>>x;end creates the session s on channel a, and continues as participant 2 out of 2. Then the process receives a message on channel 1 in session s, stores the value in the variable 'x', and then the process ends.
In this example, the channel 'a' can no longer use the protocol Gend since a message will be sent over the created session. Therefore the channel is declared as (nu a: 1=>2:1<Int>;Gend) which means that first participant 1 sends a message with an integer to participant 2 on channel 1, and then the protocol is completed.
A simple server
(nu a : 1=>2:1
{ ^sum: 1=>2:1<Int>;
1=>2:1<Int>;
2=>1:2<Int>;
Gend,
^mult:1=>2:1<Int>;
1=>2:1<Int>;
2=>1:2<Int>;
Gend,
^neg: 1=>2:1<Int>;
2=>1:2<Int>;
Gend
})
( def X(var: Int) =
link(2,a,s,2);
( X(var)
| s[1] >>
{ ^sum: s[1] >> x;
s[1] >> y;
s[2] << x+y;
end,
^mult:s[1] >> x;
s[1] >> y;
s[2] << x*y;
end,
^neg: s[1] >> x;
s[2] << 0-x;
end
}
)
in X(0)
| link(2,a,s,1);
s[1] << ^mult;
s[1] << 5;
s[1] << 3;
s[2] >> x;
link(2,a,s,1);
s[1] << ^sum;
s[1] << x;
s[1] << x;
s[2] >> x;
link(2,a,s,1);
s[1] << ^neg;
s[1] << x;
s[2] >> x;
end
)
The above code consiste of two processes, but lets start with the protocol they use to communicate.
First participant 1 (the client) sends a message to participant number two (the server) on channel 1.
This message selects between three ways the communication can continue, identified by three labels.
If the client sends the label ^sum or ^mult then the client must send two integers to the server on channel 1 before the server sends an integer to the client on channel 2.
If the client sends the label ^neg then the client must send an integers to the server on channel 1 before the server sends an integer to the client on channel 2.
The first process is the server. It creates the session s over channel a, and continues as participant 2.
As soon as the session is created, it forks into two processes, where the first waits for a new connection, and the second completes the new session.
The session is completed by branching on channel 1. This means that it receives a label, and how it continues is based on the received label.
If the label ^sum is received, it receives two integers on channel 1, and sends their sum on channel 2.
If the label ^mult is received, it receives two integers on channel 1, and sends their product on channel 2.
If the label ^neg is received, it receives one integer on channel 1, and sends the negated value on channel 2.
The second process acts as the client. By connecting to the server three times, it calculates the value of -((5*3)+(5*3)).
Persistent Server
(nu a : rec $server.
1=>2:1
{ ^add: 1=>2:1<Int>;
$server,
^mult:1=>2:1<Int>;
$server,
^neg: $server,
^done:2=>1:2<Int>;
Gend
})
( def Fork(id: Int) =
link(2,a,s,2);
( Fork(id+1)
| def Server(s: rec %server.
1 >>
{ ^add: 1>><Int>;
%server,
^mult:1>><Int>;
%server,
^neg: %server,
^done:2<<<Int>;
Lend
}@(2of2),
v: Int) =
s[1] >>
{ ^add: s[1] >> x;
Server(s,v+x),
^mult:s[1] >> x;
Server(s,v*x),
^neg: Server(s,0-v),
^done:s[2]<<v;
end
}
in Server(s,0)
)
in Fork(1)
| link(2,a,s,1);
s[1] << ^add;
s[1] << 5;
s[1] << ^mult;
s[1] << 3;
s[1] << ^mult;
s[1] << 2;
s[1] << ^neg;
s[1] << ^done;
s[2] >> x;
end
)
The above example is a calculation server, and a client that performs the same calculation as the previous example.
The difference from the previous example is that it is no longer necessary to connect to the server three times to perform the calculation.
In stead of ending the connection when the first calculation has been performed, the connection continues to with calculations, until the label ^done chosen, after which the server sends the accumulated result to the client and the session ends.
Notice that this change requires the session to be recursive.
Guessing game
(nu a: 1=>3:1<Bool>;
2=>3:2<Bool>;
3=>1:3<String>;
3=>2:4<String>;
Gend)
( // The judge
link(3,a,s,3);
s[1] >> v1;
s[2] >> v2;
if (v1 and not v2) or (v2 and not v1) // Has player 2 won
then
( s[3] << "Sorry, player 2 has won";
s[4] << "Congratulations";
end
)
else
( s[3] << "Congratulations";
s[4] << "Sorry, player 1 has won";
end
)
| // Player 1
link(3,a,s,1);
s[1] << true;
s[3] >> x;
end
| // Player 2
link(3,a,s,2);
s[2] << false;
s[4] >> x;
end
)
In this example two players each sends a boolean value to a judge. The judge decides who has won the game depending on both values, and sends the results to the players. This example shows how simple it is to write sessions with more than two participants.
Symmetric Sumtypes
Social interactions are interactions among people as well as human organisations, as opposed to interactions among computer processes.
Social interactions include workflow models and various cooperation models, and serve as a basis of many application-level protocols in computing such as healthcare and financial protocols. Just like their computer counterparts, social interactions are often highly structured, coming from the underlying social, economic and legal concerns.
There is richness in social interaction structures, stemming from diverse collaborative patterns people and human organisations can exhibit. One of such pattern is for multiple participants in an interaction to collectively decide on one of the possible choices, as found in many implicit and explicit group-based agreements.
The essence of this interaction pattern is a phase inside a conversation where a group of participants collectively wish to decide on one of the possible choices, and when they decide, they collectively commit to that option. One might call such an interaction pattern, symmetric synchronisation because all the participants are equal in the decision-making.
Apims supports symmetric synchronisation in sessions, and the protocols are described by symmetric sum types.
Synchronization
Apims represents a specific social interaction, best described as a plenum decision,
where all the participants must agree on one ofApims supports a simple kind of
social interaction, where a choice is made my agreement between the participants in a session.
This is expressed using a sync process, where a number of process must continue with a common label.
A synch process has the form
synch(n,t) {li: Pi}
and is interpreted as the process participating in a plenum decision between n processes in the session t reaching a common decision li for some i. Afterwards the process proceeds as described in Pi.
Sum Types
In order to describe the plenum decision behaviour, and allow synchronisation processes, Apims includes Symmetric Sum Types.
Symmetric sum types are of the form
{ li: Gi }
where there is at least one label li of the form #name (starting with a ^).
the labels starting with ^ are called the mandatory labels (M), and the
labels starting with # are called the optional labels (L).
The mandatory and must be accepted by all the participants.
The well-typed processes behave well in the way that they can always agree on some branch (thus they never disagree), and each process will not skip a synchronisation, or use a synchronisation that is not described in the protocol.
Example
The synchronisation and sum types are explained in the paper on Symmetric Sum Types, but we give a small example here, to explain how they work in Apims.
// The Choreography
// Patient: 1
// Doctor: 2
// Nurse: 3
(nu a : { #case1: 1=>2:1<String>;
2=>1:2<String>;
2=>1:3<String>;
Gend,
^case2: 1=>3:1<String>;
2=>1:2<String>;
2=>1:3<String>;
Gend,
#case3: 1=>2:1<String>;
3=>1:2<String>;
2=>1:3<String>;
Gend,
#case4: 1=>3:1<String>;
3=>1:2<String>;
2=>1:3<String>;
Gend })
( // The Patient
link(3,a,t,1);
sync(3,t)
{ #case1: t[1]<<"headache";
t[2]>>time;
t[3]>>result;
end,
^case2: t[1]<<"headache";
t[2]>>time;
t[3]>>result;
end,
#case3: t[1]<<"headache";
t[2]>>time;
t[3]>>result;
end,
#case4: t[1]<<"headache";
t[2]>>time;
t[3]>>result;
end
}
| // The Doctor
link(3,a,s,2);
sync(3,s)
{ #case1: s[1]>>data;
s[2]<<"now";
s[3]<<"diagnose: concussion";
end,
^case2: s[2]<<"now";
s[3]<<"diagnose: concussion";
end,
#case4: s[3]<<"diagnose: consussion";
end
}
| // The Nurse
link(3,a,r,3);
sync(3,r)
{ #case1: end,
^case2: r[1]>>data;
end,
#case3: r[2]<<"now";
end
}
)
This example first describes a choreography, explaining how three participants (a patient, a doctor and a nurse) cooperates, where they first agree on one of four cases, and then continues with the agreed case. Then the implementation of each participant is given, where the doctor does not accept the third case, and the nurse does not accept the fourth case. This means that the cases that can be selected are the mandatory case (case two) and case 1.
User Interaction
Under construction!
// The Choreography
// Patient: 1
// Doctor: 2
// Nurse: 3
(nu a: { ^Pdata: 1=>2:2<String>;1=>3:3<String>;rec $stateD.
{ ^Pdata: 1=>2:2<String>;1=>3:3<String>;$stateD,
^Dschedule: 2=>1:1<String>;2=>3:3<String>;rec $stateDS.
{ ^Pdata: 1=>2:2<String>;1=>3:3<String>;$stateD,
^Dschedule: 2=>1:1<String>;2=>3:3<String>;$stateDS,
^Nschedule: 3=>1:1<String>;3=>2:2<String>;$stateDS,
^Dresult: 2=>1:1<String>;Gend
},
^Nschedule: 3=>1:1<String>;3=>2:2<String>;rec $stateDS.
{ ^Pdata: 1=>2:2<String>;1=>3:3<String>;$stateD,
^Dschedule: 2=>1:1<String>;2=>3:3<String>;$stateDS,
^Nschedule: 3=>1:1<String>;3=>2:2<String>;$stateDS,
^Dresult: 2=>1:1<String>;Gend
}
}
})
( // Patient
link(3,a,s,1);
guisync(3,s,1)
{ ^Pdata(symptoms: String):
guivalue(3,s,1,"symptoms",symptoms);
s[2]<<symptoms;
s[3]<<symptoms;
def StateD(s: rec %stateD.
{ ^Dschedule: 1>><String>;rec %stateDS.
{ ^Dresult: 1>><String>;Lend,
^Dschedule: 1>><String>;%stateDS,
^Nschedule: 1>><String>;%stateDS,
^Pdata: 2<<<String>;3<<<String>;%stateD
},
^Nschedule: 1>><String>;rec %stateDS.
{ ^Dresult: 1>><String>;Lend,
^Dschedule: 1>><String>;%stateDS,
^Nschedule: 1>><String>;%stateDS,
^Pdata: 2<<<String>;3<<<String>;%stateD
},
^Pdata: 2<<<String>;3<<<String>;%stateD
}@(1 of 3)) =
def StateDS(s: rec %stateDS.
{ ^Dresult: 1>><String>;Lend,
^Dschedule: 1>><String>;%stateDS,
^Nschedule: 1>><String>;%stateDS,
^Pdata: 2<<<String>;3<<<String>;rec %stateD.
{ ^Dschedule: 1>><String>;rec %stateDS.
{ ^Dresult: 1>><String>;Lend,
^Dschedule: 1>><String>;%stateDS,
^Nschedule: 1>><String>;%stateDS,
^Pdata: 2<<<String>;3<<<String>;%stateD
},
^Nschedule: 1>><String>;rec %stateDS.
{ ^Dresult: 1>><String>;Lend,
^Dschedule: 1>><String>;%stateDS,
^Nschedule: 1>><String>;%stateDS,
^Pdata: 2<<<String>;3<<<String>;%stateD
},
^Pdata: 2<<<String>;3<<<String>;%stateD
}
}@(1 of 3)) =
guisync(3,s,1)
{ ^Pdata(symptoms: String):
guivalue(3,s,1,"symptoms",symptoms);
s[2]<<symptoms;
s[3]<<symptoms;
StateD(s),
^Nschedule():
s[1]>>schedule;
guivalue(3,s,1,"schedule",schedule);
StateDS(s),
^Dschedule():
s[1]>>schedule;
guivalue(3,s,1,"schedule",schedule);
StateDS(s),
^Dresult():
s[1]>>result;
guivalue(3,s,1,"result",result);
end
}
in guisync(3,s,1)
{ ^Pdata(symptoms: String):
guivalue(3,s,1,"symptoms",symptoms);
s[2]<<symptoms;
s[3]<<symptoms;
StateD(s),
^Dschedule():
s[1]>>schedule;
guivalue(3,s,1,"schedule",schedule);
StateDS(s),
^Nschedule():
s[1]>>schedule;
guivalue(3,s,1,"schedule",schedule);
StateDS(s)
}
in StateD(s)
}
| // Doctor
link(3,a,s,2);
guisync(3,s,2)
{ ^Pdata():
s[2]>>symptoms;
guivalue(3,s,2,"symptoms",symptoms);
def StateD(s: rec %stateD.
{ ^Dschedule: 1<<<String>;3<<<String>;rec %stateDS.
{ ^Dresult: 1<<<String>;Lend,
^Dschedule: 1<<<String>;3<<<String>;%stateDS,
^Nschedule: 2>><String>;%stateDS,
^Pdata: 2>><String>;%stateD
},
^Nschedule: 2>><String>;rec %stateDS.
{ ^Dresult: 1<<<String>;Lend,
^Dschedule: 1<<<String>;3<<<String>;%stateDS,
^Nschedule: 2>><String>;%stateDS,
^Pdata: 2>><String>;%stateD
},
^Pdata: 2>><String>;%stateD
}@(2 of 3)) =
def StateDS(s: rec %stateDS.
{ ^Dresult: 1<<<String>;Lend,
^Dschedule: 1<<<String>;3<<<String>;%stateDS,
^Nschedule: 2>><String>;%stateDS,
^Pdata: 2>><String>;rec %stateD.
{ ^Dschedule: 1<<<String>;3<<<String>;rec %stateDS.
{ ^Dresult: 1<<<String>;Lend,
^Dschedule: 1<<<String>;3<<<String>;%stateDS,
^Nschedule: 2>><String>;%stateDS,
^Pdata: 2>><String>;%stateD
},
^Nschedule: 2>><String>;rec %stateDS.
{ ^Dresult: 1<<<String>;Lend,
^Dschedule: 1<<<String>;3<<<String>;%stateDS,
^Nschedule: 2>><String>;%stateDS,
^Pdata: 2>><String>;%stateD
},
^Pdata: 2>><String>;%stateD
}
}@(2 of 3)) =
guisync(3,s,2)
{ ^Pdata():
s[2]>>symptoms;
guivalue(3,s,2,"symptoms",symptoms);
StateD(s),
^Nschedule():
s[2]>>schedule;
guivalue(3,s,2,"schedule",schedule);
StateDS(s),
^Dschedule(schedule: String):
guivalue(3,s,2,"schedule",schedule);
s[1]<<schedule;
s[3]<<schedule;
StateDS(s),
^Dresult(result: String):
guivalue(3,s,2,"result",result);
s[1]<<result;
end
}
in guisync(3,s,2)
{ ^Pdata():
s[2]>>symptoms;
guivalue(3,s,2,"symptoms",symptoms);
StateD(s),
^Dschedule(schedule: String):
guivalue(3,s,2,"schedule",schedule);
s[1]<<schedule;
s[3]<<schedule;
StateDS(s),
^Nschedule():
s[2]>>schedule;
guivalue(3,s,2,"schedule",schedule);
StateDS(s)
}
in StateD(s)
}
| // Nurse
link(3,a,s,3);
guisync(3,s,3)
{ ^Pdata():
s[3]>>symptoms;
guivalue(3,s,3,"symptoms",symptoms);
def StateD(s: rec %stateD.
{ ^Dschedule: 3>><String>;rec %stateDS.
{ ^Dresult: Lend,
^Dschedule: 3>><String>;%stateDS,
^Nschedule: 1<<<String>;2<<<String>;%stateDS,
^Pdata: 3>><String>;%stateD
},
^Nschedule: 1<<<String>;2<<<String>;rec %stateDS.
{ ^Dresult: Lend,
^Dschedule: 3>><String>;%stateDS,
^Nschedule: 1<<<String>;2<<<String>;%stateDS,
^Pdata: 3>><String>;%stateD
},
^Pdata: 3>><String>;%stateD
}@(3 of 3)) =
def StateDS(s: rec %stateDS.
{ ^Dresult: Lend,
^Dschedule: 3>><String>;%stateDS,
^Nschedule: 1<<<String>;2<<<String>;%stateDS,
^Pdata: 3>><String>;rec %stateD.
{ ^Dschedule: 3>><String>;rec %stateDS.
{ ^Dresult: Lend,
^Dschedule: 3>><String>;%stateDS,
^Nschedule: 1<<<String>;2<<<String>;%stateDS,
^Pdata: 3>><String>;%stateD
},
^Nschedule: 1<<<String>;2<<<String>;rec %stateDS.
{ ^Dresult: Lend,
^Dschedule: 3>><String>;%stateDS,
^Nschedule: 1<<<String>;2<<<String>;%stateDS,
^Pdata: 3>><String>;%stateD
},
^Pdata: 3>><String>;%stateD
}
}@(3 of 3)) =
guisync(3,s,3)
{ ^Pdata():
s[3]>>symptoms;
guivalue(3,s,3,"symptoms",symptoms);
StateD(s),
^Nschedule(schedule: String):
guivalue(3,s,3,"schedule",schedule);
s[1]<<schedule;
s[2]<<schedule;
StateDS(s),
^Dschedule():
s[3]>>schedule;
guivalue(3,s,3,"schedule",schedule);
StateDS(s),
^Dresult():
end
}
in guisync(3,s,3)
{ ^Pdata():
s[3]>>symptoms;
guivalue(3,s,3,"symptoms",symptoms);
StateD(s),
^Dschedule():
s[3]>>schedule;
guivalue(3,s,3,"schedule",schedule);
StateDS(s),
^Nschedule(schedule: String):
guivalue(3,s,3,"schedule",schedule);
s[1]<<schedule;
s[2]<<schedule;
StateDS(s)
}
in StateD(s)
}
)
