M-PICT

From FSL
Jump to: navigation, search
a Pi-calculus implementation in Maude
by Marcello D'Amorim and Traian Florin Șerbănuță

Contents

Introduction

Pict is an implementation language for the Pi-calculus. As such, it has a very small core, takes channels as first-class citizens, and expresses concurrency in an algebraic manner. A key feature of Pict is that communication is asyncronuous.

Pict-M is an executabale rewrite theory for a simplified version of Pict. We use Maude as a specification language and rewrite engine.

Basic Pict Constructs

In Pict one can represent processes. A process P can be

  • a paralel composition of other proceses ( \{ P_1 \mid P_2 \mid \ldots \mid P_n \} ) ;
  • a send expression ( C ! V ) which stands for sending the message V through the channel C ;
  • a receive expression ( C ? Pat = Q ) which stands for receiving a message matching the pattern Pat through the channel C, and executing the process Q with the variable in Pat being bound to the values they were matched to in the scope of P ;
  • a receive expression having a server-like behaviour; ( C ?* Pat = Q ) which receives a message on C and treats it (match and bind) but also waits for another (like spawning a new thread) request.

The construct new C P allows one to declare a channel C in the scope of the process P.

The type of channels denote the kind of information they are allowed to send or receive. For instance ^[ Integer ^[ ^[] String ] ] is a channel type which operates on integers and a channel with type ^ [ ^[] String ].

Basic Pict Values

Channel is the basic value of Pict. That means one can send and receive channels over channels. Similarly to lambda-calculus, primitive types can be encoded in Pi-calculus (and in Pict as well).

We have integers, booleans and strings as built-ins and the operation on them (also built-in) are implemented through channels. For example + is a channel which waits for a tripple [i j c] were i and j should be integers and sends through the channel c their sum. This illustrates how functions can be encoded: as processes which implement a server-like receive expression waiting for parameters and a channel where the result should be put.

PICT By Examples

Hello World!
print ! s("Hello World!")
"Hello World" or "World Hello"?
{
  print ! s("Hello")
  | 
  print ! s("World")
}
"Hello World" with syncronizaton
new 'c : ^ [] {
  pr ! [s("Hello") 'c]
  |
  'c ? [] = print ! s("World")
}
An additive memory cell
new 'mcell : ^ Int 
{
  'mcell ! i(0)
  |
  new 'add : ^ Int 
  new 'query : ^ ^ Int
  {
    'add ?* 'i : Int = 
      'mcell ? 'v : Int =
        + ! ['i 'v 'mcell]
    | 
    'query ?* 'c : ^ Int =
      'mcell  ? 'v : Int = {
        'mcell ! 'v
        |
        'c ! 'v
      }
    |
    'add ! i(10)
    |
    'add ! i(20)
    | 
    'add ! i(30)
    |
    'query ! printi 
  }
}

Type-Checker

A simple, context-insensitive, syntax-directed type-checker was defined using a continuation style by collecting constraints (extending the environment) when pattern matching or declaring types, and checking when sending messages over channels.

The sole purpose of this analysis is to verify if the use of patterns are correct. We did not implement subtyping or type inference.

Type-checking send
ceq tc ( [ X ! V @ TE ] -> K ) = tc( K )
  if T := type(V,TE) /\ T' := TE[X] /\  T' == ^ T .

Semantics

We have used a continuation-based approach to define the semantics.

Channels values are similar to "references". This allows them to be passed through other channels and avoids alpha-conversion at the expense of creating environments for processes.

In constrast to receive, the semantics of send is non-blocking. To give semantics to asynchronous communication we allow channels to "hold" multiple values (as a multi-set). The semantics for send adds an element to the multi-set while that of receive "choose" non-deterministically (through rewrite rules) an element from the channel. We took this decision in order to have fewer rewrite rules.

Send is defined equationally, therefore competing sends are term confluent. Receive, on the other hand, needs to be defined as a rewrite rule due to its blocking semantics.

Using search to find deadlocks

Dining Philosophers
 new '0 : Int new '1 : ^ Bool new '2 : ^ [] { 
   '0 ? [* : String] =  
     '1 ? [] = 
       new 'sync {
         pr ! [ s("first eats") 'sync ] | 'sync ? [] = { '0 ! [b(false)] | '1 ! [] }
       } |
   '1 ? [] =  
     '2 ? [] = 
       new 'sync {
         pr ! [ s("second eats") 'sync ] | 'sync ? [] = { '1 ! [] | '2 ! [] }
       } |
   '2 ? [] =  
     '0 ? [* : Int] = 
       new 'sync {
         pr ! [ s("third eats") 'sync ] | 'sync ? [] = { '2 ! [] | '0 ! [b(true)] }
       } |
   '0 ! [i(5)] |
   '1 ! [] |
   '2 ! []
 }

The deadlock state is

 [* nc(3) c(< prCh,empty > < printCh,empty > < printiCh,
   empty > < priCh,empty > < readCh,empty > < &Ch,empty > < |Ch,empty > < !Ch,
   empty > < +Ch,empty > < -Ch,empty > < *Ch,empty > < /Ch,empty > < %Ch,empty
   > < <=Ch,empty > < >=Ch,empty > < =Ch,empty > < <>Ch,empty > <
   int2stringCh,empty > < loc(0),empty > < loc(1),empty > < loc(2),empty >) p(
   nl(3) e(['0,loc(0)] ['1,loc(1)] ['2,loc(2)] [read,readCh] [pr,prCh] [pri,
   priCh] [print,printCh] [printi,printiCh] [&&,&Ch] [||,|Ch] [~,!Ch] [+,+Ch]
   [-,-Ch] [**,*Ch] [/,/Ch] [%,%Ch] [<=,<=Ch] [>=,>=Ch] [==,=Ch] [<>,<>Ch] [
   int2string,int2stringCh]) m([prCh,ch(prCh)] [printCh,ch(printCh)] [
   printiCh,ch(printiCh)] [priCh,ch(priCh)] [readCh,ch(readCh)] [&Ch,ch(&Ch)]
   [|Ch,ch(|Ch)] [!Ch,ch(!Ch)] [+Ch,ch(+Ch)] [-Ch,ch(-Ch)] [*Ch,ch(*Ch)] [/Ch,
   ch(/Ch)] [%Ch,ch(%Ch)] [<=Ch,ch(<=Ch)] [>=Ch,ch(>=Ch)] [=Ch,ch(=Ch)] [<>Ch,
   ch(<>Ch)] [int2stringCh,ch(int2stringCh)] [loc(0),ch(loc(0))] [loc(1),ch(
   loc(1))] [loc(2),ch(loc(2))]) k(ch(loc(0)) -> receive -> bindTo([* : Int])
   -> new 'sync {pr ! [s("third eats") 'sync] | 'sync ? [] = {'0 ! [b(true)] |
   '2 ! []}})) p(nl(3) e(['0,loc(0)] ['1,loc(1)] ['2,loc(2)] [read,readCh] [
   pr,prCh] [pri,priCh] [print,printCh] [printi,printiCh] [&&,&Ch] [||,|Ch] [
   ~,!Ch] [+,+Ch] [-,-Ch] [**,*Ch] [/,/Ch] [%,%Ch] [<=,<=Ch] [>=,>=Ch] [==,
   =Ch] [<>,<>Ch] [int2string,int2stringCh]) m([prCh,ch(prCh)] [printCh,ch(
   printCh)] [printiCh,ch(printiCh)] [priCh,ch(priCh)] [readCh,ch(readCh)] [
   &Ch,ch(&Ch)] [|Ch,ch(|Ch)] [!Ch,ch(!Ch)] [+Ch,ch(+Ch)] [-Ch,ch(-Ch)] [*Ch,
   ch(*Ch)] [/Ch,ch(/Ch)] [%Ch,ch(%Ch)] [<=Ch,ch(<=Ch)] [>=Ch,ch(>=Ch)] [=Ch,
   ch(=Ch)] [<>Ch,ch(<>Ch)] [int2stringCh,ch(int2stringCh)] [loc(0),ch(loc(
   0))] [loc(1),ch(loc(1))] [loc(2),ch(loc(2))]) k(ch(loc(1)) -> receive ->
   bindTo([]) -> new 'sync {pr ! [s("first eats") 'sync] | 'sync ? [] = {'0 !
   [b(false)] | '1 ! []}})) p(nl(3) e(['0,loc(0)] ['1,loc(1)] ['2,loc(2)] [
   read,readCh] [pr,prCh] [pri,priCh] [print,printCh] [printi,printiCh] [&&,
   &Ch] [||,|Ch] [~,!Ch] [+,+Ch] [-,-Ch] [**,*Ch] [/,/Ch] [%,%Ch] [<=,<=Ch] [
   >=,>=Ch] [==,=Ch] [<>,<>Ch] [int2string,int2stringCh]) m([prCh,ch(prCh)] [
   printCh,ch(printCh)] [printiCh,ch(printiCh)] [priCh,ch(priCh)] [readCh,ch(
   readCh)] [&Ch,ch(&Ch)] [|Ch,ch(|Ch)] [!Ch,ch(!Ch)] [+Ch,ch(+Ch)] [-Ch,ch(
   -Ch)] [*Ch,ch(*Ch)] [/Ch,ch(/Ch)] [%Ch,ch(%Ch)] [<=Ch,ch(<=Ch)] [>=Ch,ch(
   >=Ch)] [=Ch,ch(=Ch)] [<>Ch,ch(<>Ch)] [int2stringCh,ch(int2stringCh)] [loc(
   0),ch(loc(0))] [loc(1),ch(loc(1))] [loc(2),ch(loc(2))]) k(ch(loc(2)) ->
   receive -> bindTo([]) -> new 'sync {pr ! [s("second eats") 'sync] | 'sync ?
   [] = {'1 ! [] | '2 ! []}})) i(nil) o(nil) *]

Links

Our implementation
Syntax
Type Checker
Semantics
Dining Philosophers
Additive memory cell
Pict resources
Home page
Pict documentation
Personal tools
Namespaces

Variants
Actions
Navigation