Concurrence et Mobilité
Programmation concurrente et
fonctionnelle: CML et JoCaml

Georges Gonthier
INRIA Rocquencourt
Georges.Gonthier@inria.fr

Slide: 1

1. de CSP à CCS à CML à JoCaml
2. événements, canaux
3. concurrence
4. tampons
5. diffusion
6. concurrence et graphique : eXene
7. sémantique
8. JoCaml

Slide: 2

• Communicating Sequential Processes.
• Ensemble statique de processus séquentiels.
• Choix non-déterministe de Dijkstra.
• Communication explicite et synchrone de processus à processus.

Slide: 3

• Calculus of Communicating Systems.
• La communication s'effectue sur des canaux.
• Pas de notion statique de processus.
• Opérateurs de choix et de concurrence.
• Equivalence observationnelle ® algèbre.
• Pas de passage de valeur (voir le p-calcul).

Slide: 4

• Concurrent ML
• Basé sur Standard ML, mais existe aussi en bibliothèque O'Caml.
• Les canaux sont des valeurs.
• Les opérations sur les canaux sont des valeurs (événements).
• Les canaux transmettent des valeurs.
• Les événements peuvent être synchronisés lors de l'évaluation des valeurs.
• L'évaluation des valeurs peut être lancée de façon asynchrone.

Slide: 5

• Fondé sur le Join-calcul (voir cours 3).
• Basé sur O'Caml.
• Etend le modèle d'exécution avec des fonctions concurrentes.
• Exécution asynchrone, processus.
• Synchronisation par filtrage.
• Extension à la programmation distribuée et mobile.

Slide: 6

type 'a event

val sync   : 'a event -> 'a
val select : 'a event list -> 'a
val poll   : 'a event -> 'a option

val choose : 'a event list -> 'a event
val guard : (unit -> 'a event) -> 'a event

val wrap : ('a event * ('a -> 'b)) -> 'b event
val wrapHandler : ('a event * (exn -> 'a)) -> 'a event
val wrapAbort : ('a event * (unit -> unit)) -> 'a event

val always : 'a -> 'a event

Slide: 7

type 'a chan

val channel : unit -> 'a chan

val send   : ('a chan * 'a) -> unit
val accept : 'a chan -> 'a

val sameChannel : ('a chan * 'a chan) -> bool

val transmit  : ('a chan * 'a) -> unit event
val receive   : 'a chan -> 'a event

Slide: 8

type thread_id
val spawn : (unit -> unit) -> thread_id
val yield : unit -> unit
val exit : unit -> 'a
val threadWait : thread_id -> unit event

(** condition variables **)
type 'a cond_var
val condVar : unit -> 'a cond_var
val writeVar : ('a cond_var * 'a) -> unit
exception WriteTwice
val readVar : 'a cond_var -> 'a
val readVarEvt : 'a cond_var -> 'a event

Slide: 9

datatype 'a buffer_chan =
  BC of {inch : 'a chan, outch : 'a chan}

fun buffer () = let
  val inCh = channel() and outCh = channel()
  fun loop ([], []) = loop([accept inCh], [])
    | loop (front as (x::r), rear) = select [
        wrap (receive inCh, fn y => loop(front, y::rear)),
        wrap (transmit(outCh, x), fn () => loop(r, rear))]
    | loop ([], rear) = loop(List.rev rear, [])
  in
    spawn (fn () => loop([], [])); BC{inch=inCh, outch=outCh}
  end

Slide: 10

datatype 'a mchan =
             MChan of ('a request chan * 'a event chan)
     and 'a request =
             Message of 'a | NewPort

fun newPort (MChan(reqCh, respCh)) =
  (send (reqCh, NewPort); accept respCh)

fun multicast (MChan(ch, _), m) = send (ch, Message m)

Slide: 11

fun mChannel () = let
  val reqCh = channel() and respCh = channel()
  fun mkPort outFn = let
    val buf = BC.buffer() and inCh = channel()
    fun tee () = let val m = accept inCh
                 in BC.bufferSend(buf, m); outFn m; tee() end
  in spawn tee; (fn m => send(inCh, m), BC.bufferReceive buf)
  end
  fun server outFn = let
    fun handleReq NewPort = let val (outFn', port) = mkPort outFn
                            in send (respCh, port); outFn' end
      | handleReq (Message m) = (outFn m; outFn)
    in server (sync (wrap (receive reqCh, handleReq))) end
  in spawn (fn () => server (fn _ => ())); MChan(reqCh, respCh)
  end

Slide: 12

• Utilise les canaux pour separer les flux de commandes, de requêtes, de contrôle.
• Les fenêtres peuvent filtrer les événements.
• Les événements permettent un contrôle fin du déroulement des requêtes.

Slide: 13

fun copyArea arg = let
  val replyCh = channel()
  in
    spawn (fn() => request (COPY_AREA(replyCh, arg)));
    guard (fn() => (
      case (poll (receive replyCh)) of
        (SOME rects) => always rects
       | NONE        => (flush(); receive replyCh)
        (* end case *))
  end

Slide: 14

Slide: 15

Slide: 16

Slide: 17

Slide: 18

Slide: 19

• k!v ¥^k k? ® ((),v)
• Si ev₁ ¥^k ev₂ ® (e₁,e₂), alors

  ev2 k ¥   ev1 ® (e2,e1)

  ev1 k ¥   (ev2 ®v) ® (e1,v e2)

  ev1 k ¥   (ev2 Å ev3) ® (e1,ev b   3 ; e2)

  ev1 k ¥   (ev3 Å ev2) ® (e1,ev b   3 ; e2)

  ev1 k ¥   (ev2/v) ® (e1,e2)

• (k?)^b=(k!v)^b=(), (ev®v)^b=ev^b, (ev₁ Å ev₂)^b= ev₁^b; ev₂^b, et (ev/v)^b=ev^b; spawn v

Slide: 20

Slide: 21

let def put x  | cell! _ = cell x | reply ()
     or get () | cell! x = cell x | reply x;;

spawn { cell 3 };;

print_int (get ());; (* 3 *)
put 4;;
print_int (get ());; (* 4 *)
spawn { cell 5 };;
print_int (get ());; (* 4 ou 5 *)

This document was translated from L^AT_EX by H^EV^EA.