A Shared Memory Communication Protocol

Łukasz Bieniasz-Krzywiec


na podstawie "Distributed Systems Analysis with CCS" autorstwa G. Bruns'a

Plan

Plan

Czym jest MSMIE?

Składowe systemu

Schemat Systemu

Wymagania

Uproszczenia

Plan

Zły pomysł [1/2]


Wady to opóźnienia:
  • gdy Master czeka aż Slave skończy pisać
  • gdy Slave czeka aż Master skończy czytać

Zły pomysł [2/2]



Wady to znów opóźnienia.

Plan

Dobry pomysł


Slave write

  1. Zdobądź semafor.
  2. Jeśli jest bufor newest, to zmień jego status na idle.
  3. Jeśli jest bufor slave, to zmień jego status na newest.
    Wpp. BŁĄD
  4. Jeśli jest bufor idle, to zmień jego status na slave.
    Wpp. BŁĄD
  5. Oddaj semafor.

Master Acquire

  1. Zdobądź semafor.
  2. Jeśli jest bufor newest i nie ma bufora master,
    to zmień status bufora newest na master.
  3. Jeśli jest bufor master, to zwiększ liczbę czytających procesorów.
  4. Oddaj semafor.

Master Release

  1. Zdobądź semafor.
  2. Zmniejsz liczbę czytających procesorów.
  3. Jeśli liczbę czytających procesorów == 0, to
    1. Jeśli jest bufor newest, to zmień status bufora master na idle.
    2. Wpp. zmień status bufora master na newest.
  4. Oddaj semafor.

Kilka własności

Plan

Interfejs

Bufory

Buf(s)    = 'read(s).Buf(s) + write(s').Buf(s')

Buf_i(s)  = Buf(s)[read_i/read, write_i/write]

Buffers   = Buf_1(s) | Buf_2(i) | Buf_3(i)

Counter i Semaphore

Counter(n) = (if n = 0 then zero.Counter(n)) 
           + (if n < 2 then inc.Counter(n + 1))
           + (if n > 0 then dec.Counter(n - 1))


Semaphore  = take.give.Semaphore
  
MemImage = Buffers | Counter(0) | Semaphore

Slave

Slave  = slave.Sl1


Sl1    = 'take.read_1(v1).read_2(v2).read_3(v3).Sl2((v1,v2,v3))


Sl2(B) = sum(i:{1,2,3}, if B#i = N then Sl3(B[i -> I])) 
       + if N not in {B#1, B#2, B#3} then Sl3(B)


Sl3(B) = sum(i:{1,2,3}, if B#i = S then Sl4(B[i -> N]))


Sl4(B) = sum(i:{1,2,3}, if B#i = I then Sl5(B[i -> S]))


Sl5(B) = 'write_1(B#1).'write_2(B#2).'write_3(B#3).'give.Slave

Master Acquire

Master = MA1


MA1    = 'take.read_1(v1).read_2(v2).read_3(v3).MA2((v1,v2,v3))


MA2(B) = if N in {B#1, B#2, B#3} and M not in {B#1, B#2, B#3}
         then sum(i:{1,2,3}, if B#i = N then MA3(B[i -> M]))
         else MA3(B)



MA3(B) = (if M in {B#1, B#2, B#3} then ma.'inc.MA4(B))
       + 'give.Master


MA4(B) = 'write_1(B#1).'write_2(B#2).'write_3(B#3).'give.MR1

Master Release

MR1    = mr.'take.read_1(v1).read_2(v2).read_3(v3).MR2((v1,v2,v3))


MR2(B) = 'dec.MR3(B)


MR3(B) = 'zero.(sum(i:Bid, if B#i = M
                           then (if N in {B#1, B#2, B#3} 
                                 then MR4(B[i -> I])
                                 else MR4(B[i -> N]))))
       + 'dec.'inc.MR4(B)


MR4(B) = 'write_1(B#1).'write_2(B#2).'write_3(B#3).'give.Master

Z lotu ptaka

Master_k = Master[ma_k/ma, mr_k/mr]


Msmie = (MemImage | Slave | Master_1 | Master_2) \ L

Plan

Sprawdzamy wymagania [1/2]

  1. data tearing - OK
  2. Czy Slave zawsze może pisać do bufora?
    Czy akcję slave można zawsze wykonać?

    Always(A) = max(X.A & [[-]]X)

    SlaveAlwaysPossible = Always(<<slave>>T)

    OK

Sprawdzamy wymagania [2/2]

  1. Czy Master zawsze może czytać z bufora?
    Czy akcje ma, mr można zawsze wykonać?

    MasterAlwaysPossible =
    [[slave]]Always(<<ma1,mr1>>T & <<ma2,mr2>>T)

    OK

Plan

Slave actions

  1. M({(s,l1), (n,l2), (i,l3)}, r) - slave → M({(n,l1), (s,l2), (i,l3)}, r)
  2. M({(s,l1), (n,l2), (i,l3)}, r) - slave → M({(n,l1), (i,l2), (s,l3)}, r)
  3. M({(s,l1), (i,l2)} + B', r) - slave → M({(n,l1), (s,l2)} + B', r)
    gdzie, (n,_) not in B'
  4. M({(s,l1), (n,l2)} + B', r) - slave → M({(n,l1), (s,l2)} + B', r)
    gdzie, (i,_) not in B'

Master acquire actions

Dla k = 1,2
  1. M({(m,l)} + B', r) - ma_k → M({(m,l)} + B', r + {k})
    gdzie, k not in r
  2. M({(n,l)} + B', Ø) - ma_k → M({(m,l)} + B', {k})
    gdzie, (m,_) not in B'

Master release actions

Dla k = 1,2
  1. M({(m,l)} + B', r + {k}) - mr_k → M({(m,l)} + B', r)
    gdzie, r != Ø, k not in r
  2. M({(m,l1), (n,l2)} + B', {k}) - mr_k → M({(i,l1), (n,l2)} + B', Ø)
  3. M({(m,l)} + B', {k}) - mr_k → M({(n,l)} + B', Ø)
    gdzie, (n,_) not in B'

Wersja Minimalna MSMIE

Ups...

Plan

Drobna zmiana

Dla k = 1,2
  1. M({(n,l)} + B', Ø) - ma'_k → M({(m,l)} + B', {k})
    gdzie, (m,_) not in B'

ma'_k oznacza zaczęcie czytania z bufora o statusie newest.

Zmieniona Wersja Minimalna MSMIE

Zapomniana własność

Dane zapisane przez Slave zostaną w końcu odczytane.

Nasz model nie ma tej własności, bo nie mamy żadnej pewności, że akcje Master występują.

Jeśli Master actions będą ciągle występować, to dane zapisane przez Slave zostaną w końcu odczytane.

Jak opisać tę własność formułą?

Kluczowa Formuła [1/2]

Rozważmy proces z sort równym {a, b, c}.

Kluczowa Formuła [2/2]

W naszym przypadku: 

Fair = min(X.max(Y1.<<-eps>>T & [[mr1,mr2,slave,ma2]]Y1 & [[ma1]]
             max(Y2.<<-eps>>T & [[mr1,mr2,slave,ma1]]Y2 & [[ma2]]X)));

ValuesPassed = Always([[slave]]Fair);

Plan

Nowe MSMIE

Nowe Master Acquire

  1. Jeśli nie ma bufora master, to zmień status bufora newest na master i zacznij z niego czytać.
  2. Jeśli bufor b1 ma status master i bufor b2 ma status newest i nie ma bufora old, to:
    1. zmień status bufora b1 na old,
    2. zmień status bufora b2 na master i zacznij z niego czytać.
  3. Jeśli bufor b ma status master oraz nie ma bufora newest lub jest bufor old, to zacznij czytać z bufora b.