Pravidelná sémantika - Regular semantics

Pravidelná sémantika je výpočetní termín, který popisuje jeden typ záruky poskytované datovým registrem sdíleným několika procesory v paralelním stroji nebo v síti počítačů spolupracujících. Pravidelná sémantika je definována pro proměnnou s jedním zapisovatelem, ale s více čtečkami. Tato sémantika je silnější než bezpečná sémantika, ale slabší než atomová sémantika : zaručuje, že operace zápisu mají celkový řád, který je konzistentní s real-time a že operace čtení vracejí buď hodnotu posledního zápisu dokončeného před začátkem čtení, nebo jeden z zápisů, které jsou souběžné s čtením.

Příklad

Pravidelná sémantika je slabší než linearizovatelnost. Zvažte níže uvedený příklad, kde vodorovná osa představuje čas a šipky představují interval, během kterého probíhá operace čtení nebo zápisu. Podle definice regulárního registru by třetí čtení mělo vrátit 3, protože operace čtení není souběžná s žádnou operací zápisu. Na druhé straně může druhé čtení vracet 2 nebo 3 a první čtení může vracet buď 5 nebo 2. První čtení může vracet 3 a druhé čtení může vracet 2. Toto chování by nesplňovalo atomovou sémantiku. Pravidelná sémantika je tedy slabší vlastností než atomová sémantika. Na druhou stranu Leslie Lamport prokázal, že linearizovatelný registr může být implementován z registrů s bezpečnou sémantikou , které jsou slabší než běžné registry.

Bezpečná registrace

Věta od pravidelnosti k atomičnosti

Atomová sémantika s jedním zapisovatelem pro více čtenářů (SWMR) je pravidelný registr SWMR, pokud některá z jeho historie provádění H splňuje následující vlastnost: r1 a r2 jsou libovolné dvě přečtené vyvolání: (r1 → H r2) ⇒ ¬π (r2) → H π (r1)

Než se dostaneme k důkazu, měli bychom nejprve vědět, co znamená nová / stará inverze. Jak je znázorněno na obrázku níže, při pohledu na provedení vidíme, že jediný rozdíl mezi běžným provedením a atomovým provedením je, když a = 0 a b = 1. V tomto provedení, když vezmeme v úvahu dvě přečtené vyvolání R .read () → a následovaný R.read () → b, naše první hodnota (nová hodnota) je a = 0, zatímco druhá hodnota (stará hodnota) je b = 1. To je vlastně hlavní rozdíl mezi atomicitou a pravidelností.

Obrázek 1

Výše uvedená věta uvádí, že regulární registr s více čtečkami s jedním zapisovatelem bez nové nebo staré inverze je atomový registr. Při pohledu na obrázek můžeme říci, že jako R.read () → a → H R.read () → b a R.write (1) → H R.write (0) není možné mít π ( R.read () → b) = R.write (1) a π (R.read () → a) = R.write (0), pokud je provedení atomové. Abychom prokázali výše uvedenou větu, měli bychom nejprve dokázat, že registr je bezpečný, dále bychom měli ukázat, že registr je pravidelný, a na konci bychom měli ukázat, že registr neumožňuje novou / starou inverzi, která dokazuje atomicitu. Podle definice atomového registru víme, že atomový registr s více čtečkami s jedním zapisovačem je pravidelný a splňuje vlastnost bez nové / staré inverze. Musíme tedy jen ukázat, že běžný registr bez nové / staré inverze je atomový.

Víme, že pro každé dvě vyvolání čtení (r1 a r2) je registr pravidelný a neexistuje nová / stará inverze (r1 → H r2) ⇒sn (π (r1)) ≤ sn (π (r2)). Pro jakékoli provedení (M) existuje celková objednávka (S), která zahrnuje stejné vyvolání operací. Můžeme konstatovat, že S je postaveno následovně: vycházíme z celkového pořadí operací zápisu a operaci čtení vložíme následovně: první: Operace čtení (r) se vloží za přidruženou operaci zápisu (π (r)) Druhá: Pokud mají dvě operace čtení (r1, r2) stejné (sn (r1) = sn (r2)), pak nejprve vložte operaci, která začíná jako první při provádění. S zahrnuje veškeré vyvolání operace M, z čehož vyplývá, že S a M jsou ekvivalentní. Vzhledem k tomu, že všechny operace jsou seřazeny na základě jejich pořadových čísel, je mírně celková objednávka. Kromě toho je toto celkové pořadí provedením M pouze přidává pořadí operací, které se překrývají v M. Pokud nedochází k překrývání mezi operacemi čtení a zápisu, není žádný rozdíl mezi pravidelností a atomicitou. Nakonec můžeme konstatovat, že S je legální, protože každá operace čtení získá poslední zapsanou hodnotu, která předchází v celkovém pořadí. Proto je odpovídající historie linearizovatelná. Protože toto uvažování se nespoléhá na konkrétní historii H, znamená to, že registr je atomový. Vzhledem k tomu, že atomicita (linearizovatelnost) je místní vlastnost, můžeme konstatovat, že sada pravidelných registrů SWMR se chová atomicky, jakmile každý z nich splňuje vlastnost žádná nová / stará inverze.

Reference