functional thursday ＃73

發表於 | 分類於 | | times
字數統計: 660 word(s) | 閱讀時長 ≈ 4 min(s)
π-calculas 不負責任筆記



Concurrency vs Parallelism

compile normal program into parallelism program? Hard!

make changes on program as little as possible!

  • parallelism ⇒ multi-processor, multi-processes
  • concurrency ⇒ single-processor, multi-processes

make write wrong program harder?

Concurrent model

  • CSP ⇒ process - process event
  • π-calculas ⇒ channel - channel message passing

process algebra

π-calculas is the most complex one, but useful

π-calculas

Send and receive are atomic operation

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
SquareServer = c(x) . c<x^2> . SquareServer
-- SquareServer is recursive

P1 = c<3> . c(x) . ∅
-- a client want to get square of 3

P2 = c<4> . c(y) . ∅
-- a client want to get square of 4

main = SquareServer | P1
-- run SquareServer, P1 at the smae time.

let < > = send
let ( ) = receive
let  c  = channel
let  .  = end
let  ∅  = stop

Error?

1
2
3
4
5
SumServer = C(x) . C(y) . C(x + y) . SumServer
P1 = C<3> . C<5> . C(x) . ∅
P1 = C<4> . C<6> . C(x) . ∅

-- may cause race or deadlock

Give every process unique channel!

1
2
3
4
5
6
SumServer = νd . c<d> . d(x) . d(y) . d<x + y> . SumServer
P1 = c(d) . d<3> . d<5> . d(x) . ∅
P2 = c(d) . d<6> . d<4> . d(x) . ∅

SumServer | P2 | P1
-- no race or deadlock!

More powerful server?

1
2
SumServer = (νd . c<d> . d(x) . d(y) . d<x + y> . ∅) | SumServer
-- calculate and provide other service at the same time!

Define such operator

1
P = !Q = Q | P = Q | Q | Q | ...

Math server

1
2
3
4
5
6
7
8
9
10
-- ⊳ select
-- ⊲ choice

MathServer = νc . ms<c>

where
   c ⊳ { ADD → c(x) . c(y) . c<x + y> . ∅;
         NEG → c(x) . c(-x) . ∅} | MathServer

user = ms(c) . c ⊲ ADD . c<3> . c<4> . c(x) . ∅

MathServer throw select operation? how?

1
2
3
4
5
6
7
8
9
10
MathServer = νc . ms<c> . worker c | MathServer

worker c = c ⊳ {
     ADD → c(x) . c(y) . c<x + y> . worker c;
     NEG → c(x) . c(-x) . worker c;
     END → ∅} | MathServer

-- worker need to receive "c" ?! function call?

user = ms(c) . c ⊲ ADD . c<3> . c<4> . c(x) . ∅

No function call! use a w(orker) channel to pass “c”

1
2
3
4
5
6
MathServer = νc . ms<c> . w<c> | MathServer

worker = !(w(c) . c ⊳ {
           ADD → c(x) . c(y) . c<x + y> . w<c> . ∅ ;
           NEG → c(x) . c(-x) . w<c> . ∅;
           END → ∅})

Dinning phylosophers in π-calculas

omit

Basic Rules

identity and association rule

1
2
3
4
5
(P | Q) | R ≡ P (Q | R)
P | Q ≡ Q | P
P | ∅ ≡ P

P ≡ Q ⇒ R | P == R | Q

reduction rule

1
2
proc = a<x> . P | a(y) . Q → P | Q [x / y]
-- should substitute y to x fisrt(?)
1
2
w<a> . a<3> . P | w(z) . z(x) . b<x + 3>
→ a<3> . P | a(x) . b<x + 3>

axiom relating restriction and parallel

1
2
3
4
5
6
7
8
9
(νx . P) | Q ≡ νx . (P | Q) if Q not contains x


(νa . w<a> . a<3> . P) | w(z) . z(x) . b<x + 3>
≡ νa(w <a> . a<3> . P | w(z) . z(x) . b<x + 3>)
→ νa(P | b<6>)
...
→ νa . ∅
→ ∅

Type system in π-calculas

  • process is untyped
  • channel is typed

Γ ⊢ P

Dual type

$c : (?Int . !Int . ∅)^{⊥} = !Int . ?Int . ∅$

Type inference

$\frac{Γ, x:t, y:s ⊢ P}{Γ, x:?s . t ⊢ x(y) . P}$

$\frac{Γ ⊢ y:s \quad Γ, x:t ⊢ P}{Γ, x:!s . t ⊢ x \langle y . P}$

note x:t not x:t, y:s

$\frac{Γ_{1} ⊢ P \quad Γ_{2} ⊢ Q}{Γ_{1} ∘ Γ_{2} ⊢ P | Q}$

if $x ∈ Γ_{1}$ is $t$
then $x ∈ Γ_{2}$ need to be $t^{⊥}$

type preservation

Γ ⊢ e : τ ∧ e -> e’ ⇒ Γ ⊢ e’ : τ

Γ ⊢ e : τ

  • e value
  • ∃ e’, e → e’

linear logic

cut rule

------------- EOF -------------