Damien Pous' Home Page.

GcPan: an Efficient Abstract Machine for Safe Ambients

The GcPan is an abstract machine for Safe Ambients (SA) that we developped with Daniel Hirschkoff and Davide Sangiorgi. It's an improvement of the PAN machine (P. Giannini, D. Sangiorgi, A. Valente: "Safe Ambients: abstract machine and distributed implementation"). The machine is described in this extended abstract, published in the proceedings of COORDINATION 2005, and we derive a weak bisimulation result w.r.t. the Pan in this extended version, that appeared in JLAP 2007. The correctness w.r.t. SA comes from the correctness of the PAN.

Abstract: Safe Ambients (SA) are a variant of the Ambient Calculus (AC) in which types can be used to avoid certain forms of interferences among processes called grave interferences}.
An abstract machine, called GCPAN, for a distributed implementation of typed SA is presented and studied. Our machine improves over previous proposals for executing AC, or variants of it, mainly through a better management of special agents (the forwarders), created upon code migration to transmit messages to the target location of the migration. Well-known methods (such as reference counting and union-find) are applied in order to garbage collect forwarders, thus avoiding long -- possibly distributed -- chains of forwarders, as well as avoiding useless persistent forwarders.
The proof of correctness of GCPAN, and a description of a distributed implementation of the abstract machine in OCaml are given.
Correctness is established by proving a weak bisimilarity result between GCPAN and a previous abstract machine for SA, and then appealing to the correctness of the latter machine. This is simpler than comparing GCPAN directly with SA, but it involves reasoning modulo `administrative reduction steps' in both machines and therefore standard techniques for simplifying proofs of weak bisimilarity results are not applicable.
More broadly, this study is a contribution towards understanding issues of correctness and optimisations in implementations of distributed languages encompassing mobility.

This page presents a distributed implementation of this abstract machine, written in OCaml.

1. Installation:

   Download sources or binaries there: sources, bytecode, nativecode, examples.
   In case of sources, “make” will compile the executable (“make nc” for native compilation); provided you have a standard OCaml installation (3.10 - 3.07, maybe 3.06).

   You can copy the executable “gcpan” wherever you want.

2. Usage:

   • Most useful command line options are:

     • "-pan" for emulating the original PAN abstract machine,

     • "-p port" to use the given port for external connections.

   • Then you can enter a process followed by `;;' in order to execute it.

   • Processes are standard Safe Ambients processes, with two additional capabilities:

     • `print o.P' : prints o and executes P

     • `pause p.P' : waits for a `#step p' user directive, and runs P (furthermore, `pause 3 p.P' will pause only after 3 evaluations)

     rec X.pause 3 p.(a[ in B.print toto.open_a.<o> ] | X)
     | B[ !in_B.open a | rec X.(x)print x.X ] ;;
     toto
     toto
     o
     o
     toto
     o
     #step p;;
     toto
     o
     

     (after the first pause, the pause 3 command behaves like pause).

   • In order to get sensible behaviours, processes must be well-typed: single threaded (resp. immobile) ambients names must begin with a lowercase (resp. uppercase) letter. (experimental type inference/checking is available trough the `#check P' directive).

   • `#add P;;' allows you to add the process P to the currently executed process.

   • Other directives are available:

     • #tree : prints the current tree (forwarders are represented by by <[]),
     • #stats: prints collected statistics,
     • #quit : exit,
     • #help : lists all other directives (should come quiet soon...).

   • You can also define macros:

     let o(n,'P) = n[in a| P];;
     let dup('P) = 'P | 'P;;
     dup(o(a,b[]));;
     #tree;;

3. Distributed Execution:

   • Distribution from a given site

     Run two instances of gcpan on two different machines, A and B.
     Then evaluate the process on A: `a[print a] | b@B[print b]'.
     The ambient b is evaluated at B !

     You can also run gcpan from two terminals, using option '-p 2000' on the second terminal, and evaluate the process `a[print a] | b@localhost:2000[print b]'.

   • Connection to a given site

     Evaluate `a[in_a.print hello]' on A,
     and `#addto A b[in a.print ciao]' on B.

     The latter process executes on B, but is connected to the root of A !

   • Code migration

     In the previous example, there were no code migration: both print statements are executed on the site they were typed in.

     Indeed, in the (GC)PAN, migration only occurs with OPEN moves:
     to see it, execute `a[in_a.open b] | c[in_c.print c]' on A,
     and `#addto A b[in a.print leaving.open_b.print moved.in c]' on B.

     The process `print moved.in c' migrated to A !

4. Example session: Cabs

   In this example, extracted from this paper, several clients travel between sites using cabs.

   
   Let us define some macros:

   (* Code for a site named `A' *)
   let site(A,'P) = A[!in_A | !out_A | P];;
   
   (* Code for a cab *)
   let cab() =
    cab[rec X.in_cab.open call.(A)in A.
    in_cab.open trip.(B)out A.in B.out_cab.out B.X];;
   (* Code for a client named `c', that wants to go from `A' to `B', before executing `P' *)
   let travel(c, A, B, 'P) =
     call[out c.out A.in cab.open_call.<A>]
   | out_c.in cab.(trip[out c.open_trip.<B>] | out_c.out cab.P);;
   (* Code for a client named `c', that loops between `A' and `B' *)
   let loop(c, A, B) =
    rec X.travel(c, A, B, print tic.travel(c, B, A, print tac.X));;

   Now you can run different sites and clients:

   site(Vienne, joe[travel(joe,Vienne,Lyon,print JoeAtLyon.
                    travel(joe,Lyon,Bologna,print JoeAtBologna))])
   | site(Lyon, bar[travel(bar,Lyon,Vienne,print BarAtVienne)])
   | site(Bologna, maurice[pause.loop(maurice,Bologna,Lyon)]);;

   Nothing happen since there is no cab yet...
   You can print the current state :

   #tree;;
   ?[joe[]]
   ?[bar[]]
   R@@t[call[] | call[] | Vienne[] | Lyon[] | Bologna[maurice[]]]

   (joe and bar are in wait state, which is why they appear disconnected from the main tree of ambients)
   
   Now add one (or more) cab, and print the state :

   #add cab();;
   BarAtVienne
   JoeAtLyon
   JoeAtBologna
   #tree;;
   R@@t[Bologna[maurice[] | <[joe[]]] | Vienne[<[bar[]]] | cab[] | Lyon[]]

   (The `<' in front of joe and bar are forwarders).
   
   Finally you can trigger maurice's loop:

   #step;;
   tic
   tac
   tic
   tac
   tic
   ...
   

5. Another example session: comparing the PAN and the GCPAN

   We now move a more ad-hoc example to illustrate how forwarders are managed in the GCPAN w.r.t. the PAN (this example can be found in file mariage.ml in the distribution).
   We start by defining the following agents:

   let a() = A[pause i.(!in_A | !out_A)];;
   let b() = b[pause i.in A.pause o.out A];;
   let c('P) = c[open_c | P];;

   A b agent is willing to enter and exit ambient A, while c ambients are ready to be opened. We start in an initial arbitrary configuration that consists in two trees of c nodes with A (resp. b) ambients at the leafs:

   c(c(c(a()|a()|a())|c(a()))|c(c(c(c(a())|c(a()|a()|a())|a())|c(a())|a())|c(a()|a())))
   | c(c(c(b()|b()|b())|c(b()))|c(c(c(c(b())|c(b()|b()|b())|b())|c(b())|b())|c(b()|b())));;
   #tree;;
   R@@t[
        c[
         c[c[<[A[]] | <[A[]]] |
          c[<[A[]] | c[<[A[]]] |
           c[<[A[]] | c[<[A[]] | <[A[]] | <[A[]]] | c[<[A[]]]]]]
         | c[c[<[A[]] | <[A[]] | <[A[]]] | c[<[A[]]]]]
        |
        c[
         c[c[b[] | b[]] |
          c[b[] | c[b[]] | c[b[] | c[b[] | b[] | b[]] | c[b[]]]]]
         | c[c[b[]] | c[b[] | b[] | b[]]]]]
     

   The initial state of the system is blocked. Now by adding a process that removes all c nodes, we can bring the as and bs to the toplevel, and they can interact. Let us do it, and observe the result:

   #add !open c;;
   #tree;;
   R@@t[<[<[A[]] | <[A[]] | <[A[]]] | <[<[A[]] | <[A[]]] | <[<[A[]]] |
      <[b[] | b[]] | <[<[A[]]] | <[b[]] | <[<[A[]]] | <[b[]] |
      <[<[A[]] | <[A[]] | <[A[]]] | <[b[] | b[] | b[]] | <[b[]] | <[<[A[]]] |
      <[<[A[]]] | <[b[]] | <[b[]] | <[b[] | b[] | b[]]]

   This is the situation after the opening of all c ambients: agents are blocked at the synchronisation point named i. We may observe that some forwarders have appeared, actually less than the 22 c ambients that were initially present: some c ambients were known to contain no direct subambient at the moment of the opening.
   We now use step i to let computation resume; execution will stop at the next synchronisation point, named o, and we then let the system evolve until its ending state.

   #step i;;
   #tree;;
   R@@t[<[A[]] | <[A[]] | <[A[b[] | b[] | b[] | b[] | b[]]] | <[A[b[]]] |
      <[A[b[] | b[]]] | <[A[b[]]] | <[A[b[]]] | <[A[b[]]] | <[A[b[]]] |
      <[A[b[]]] | <[A[]] | <[A[]] | <[A[]]]
   #step o;;
   #tree;;
   R@@t[<[A[]] | <[A[]] | <[A[] | b[] | b[] | b[] | b[] | b[]] | <[A[] | b[]] |
      <[A[] | b[] | b[]] | <[A[] | b[]] | <[A[] | b[]] | <[A[] | b[]] |
      <[A[] | b[]] | <[A[] | b[]] | <[A[]] | <[A[]] | <[A[]]]
   

   After the first step command, all bs have entered an A, and after the second such command, they went back out, thus generating some extra forwarders (because of the treatment of the OUT rule in GCPAN).
   
   We can examine statistics about the computation we have just been running:
   

   #stats;;
   forwarders : 16 + 0 + 13 - 16 = 13
   local messages : 239
   network messages : 0
   requests : 70
   completions : 83
   relocations : 32
   local_com : 0
   local_in : 13
   local_out : 13
   local_open : 22
   average forwarder lifetime : 0.62
   average forwarder chains length : 0.46
   average request packages size : 1.06

   16 forwarders have been created upon execution of an open capability, 0 upon an out, 13 persistent forwarders associated to an immobile ambient (all A ambients are immobile -- note that no forwarder has appeared along OUT moves because these involve exiting an immobile ambient). Out of these 29 forwarders, all 16 non-persistent ones have been garbage collected along execution.
   All 239 messages (requests, completions, etc..: see the details above) have been exchanged locally, because we ran this example on a single machine.
   Finally, we can observe that we have short-lived forwarders, and forwarder chains contraction leads to very short forwarder chains in average. The size of request messages (which in GCPAN is not bounded, in constrast with the PAN) is kept rather small.
   
   This was a GCPAN run. If we replay the same example using the PAN (option -pan), here is what we get:

   forwarders : 22 + 0 + 0 - 0 = 22
   local messages : 370
   network messages : 0
   requests : 74
   completions : 83
   relocations : 0
   local_com : 0
   local_in : 13
   local_out : 13
   local_open : 22
   average forwarder lifetime : -1.00
   average forwarder chains length : 2.20
   average request packages size : 1.00

   In the PAN, we do not create forwarders upon execution of out moves, immobile ambients are created without associated forwarder, but we do not remove any forwader: this explains the + 0 + 0 - 0 above. Moreover, we systematically create forwarders when opening an ambient, while we avoid doing so when the opened ambient is empty in the GCPAN: this is why we get 22 forwarders in the PAN.
   On this example, since we have almost twice as much forwarders as in the GCPAN, and since a lot of communication takes place between ambients, we observe much more messages in the PAN than in the GCPAN.
   The negative lifetime of forwarders simply means that all forwarders are persistent in the PAN. As expected, we observe that all request messages have the same size in the PAN, and chains are longer because no contraction mechanism is provided.
   
   A few more examples can be found in the examples/ directory in the distribution.

6. Bug reports / Feature wishes:

   They are welcome, you can reach me at Damien dot Pous at ens-lyon dot fr .