Broadcast vlastnosti: FIFO, kauzalita, atomicita

Zdrojový topic: broadcast-fifo-kauzalita

Co si pamatovat

U diagramů nejdřív rozliš, co přesně se kontroluje:

VlastnostKontrolujePorušení
FIFOpořadí zpráv od stejného odesílateleněkdo doručí m2 před m1, i když stejný odesílatel poslal m1 před m2
Kauzalitahappened-before mezi zprávaminěkdo doručí následek před příčinou
Atomicitastejné globální pořadí u všechdva procesy doručí stejné zprávy v jiném pořadí

Jedna osa rozhodování

flowchart TD
  A["Mám dvě doručené zprávy v podezřelém pořadí"] --> B{"stejný odesílatel?"}
  B -->|ano| C{"poslal je opačně?"}
  C -->|ano| D["porušení FIFO"]
  C -->|ne| E["FIFO neporušeno touto dvojicí"]
  B -->|ne| F{"existuje happened-before m1 -> m2?"}
  F -->|ano| G{"někdo doručil m2 před m1?"}
  G -->|ano| H["porušení kauzality"]
  G -->|ne| I["kauzalita neporušena touto dvojicí"]
  F -->|ne| J{"mají dva procesy jiné pořadí stejných zpráv?"}
  J -->|ano| K["porušení atomicity"]
  J -->|ne| L["bez porušení z této dvojice"]

Mini příklady porušení

FIFO

Odesílatel S pošle m1, potom m2.

ProcesDoručení
P1m1, m2
P2m2, m1

P2 porušuje FIFO, protože jde o stejný sender S.

Kauzalita

Platí m1 -> m2, například P2 poslal m2 až po přijetí m1.

ProcesDoručení
P1m1, m2
P3m2, m1

P3 porušuje kauzalitu, protože doručil následek před příčinou.

Atomicita

Zprávy nemusí být kauzálně svázané, ale atomic broadcast vyžaduje jedno globální pořadí.

ProcesDoručení
P1a, b
P2b, a

Porušení atomicity: stejné zprávy, jiné pořadí.

Zkoušková odpověď

  1. Vždy napiš, jestli řešíš deliver, ne jen recv.
  2. FIFO dokazuj nebo vyvracej jen u zpráv od stejného odesílatele.
  3. Kauzalitu dokazuj přes ->.
  4. Atomicitu dokazuj porovnáním pořadí mezi procesy.

Časté chyby

  • Říct, že atomicita plyne z FIFO. Ne, atomicita je globální pořadí.
  • Říct, že kauzalita plyne z pořadí u jednoho sendera. To je jen část kauzality.
  • Hledat porušení v nedoručených nebo jen přijatých zprávách.

Termínové zdroje