Linjäriserbarhet

I grå linjär delhistorik har processer som börjar i b inte en linjäriserbar historia eftersom b0 eller b1 kan slutföras i endera ordningen innan b2 inträffar.

I samtidig programmering är en operation (eller en uppsättning operationer) linjäriserbar om den består av en ordnad lista med anrops- och svarshändelser , som kan utökas genom att lägga till svarshändelser så att:

  1. Den utökade listan kan återuttryckas som en sekventiell historia (är serialiserbar ).
  2. Den sekventiella historiken är en delmängd av den ursprungliga oförlängda listan.

Informellt betyder detta att den omodifierade listan över händelser är linjäriserbar om och endast om dess anrop var serialiserbara, men några av svaren i serieschemat har ännu inte återkommit.

I ett samtidigt system kan processer komma åt ett delat objekt samtidigt. Eftersom flera processer har åtkomst till ett enda objekt, kan det uppstå en situation där medan en process kommer åt objektet, ändrar en annan process dess innehåll. Att göra ett system linjäriserbart är en lösning på detta problem. I ett linjäriserbart system, även om operationer överlappar på ett delat objekt, verkar varje operation ske omedelbart. Linjäriserbarhet är ett starkt korrekthetsvillkor, som begränsar vilka utdata som är möjliga när ett objekt nås av flera processer samtidigt. Det är en säkerhetsegenskap som säkerställer att verksamheten inte slutförs på ett oväntat eller oförutsägbart sätt. Om ett system är linjäriserbart tillåter det en programmerare att resonera om systemet.

Lineariserbarhetens historia

Lineariserbarhet introducerades först som en konsistensmodell av Herlihy och Wing 1987. Den omfattade mer restriktiva definitioner av atomär, som "en atomär operation är en som inte kan (eller inte) avbrytas av samtidiga operationer", som vanligtvis är vaga om när en operation anses påbörjas och avslutas.

Ett atomobjekt kan omedelbart och fullständigt förstås utifrån dess sekventiella definition, som en uppsättning operationer som löper parallellt och som alltid tycks inträffa efter varandra; inga inkonsekvenser får uppstå. Specifikt garanterar lineariserbarhet att invarianterna i ett system observeras och bevaras av alla operationer: om alla operationer individuellt bevarar en invariant, kommer systemet som helhet att göra det.

Definition av lineariserbarhet

Ett samtidigt system består av en samling processer som kommunicerar genom delade datastrukturer eller objekt. Linjäriserbarhet är viktigt i dessa samtidiga system där objekt kan nås av flera processer samtidigt och en programmerare måste kunna resonera kring de förväntade resultaten. En exekvering av ett samtidigt system resulterar i en historik , en ordnad sekvens av genomförda operationer.

En historia är en sekvens av anrop och svar gjorda av ett objekt av en uppsättning trådar eller processer. Ett anrop kan ses som början på en operation, och svaret är det signalerade slutet på den operationen. Varje anrop av en funktion kommer att ha ett efterföljande svar. Detta kan användas för att modellera vilken användning som helst av ett objekt. Anta till exempel att två trådar, A och B, båda försöker ta tag i ett lås och backar om det redan har tagits. Detta skulle modelleras som att båda trådarna anropar låsoperationen, sedan får båda trådarna ett svar, en framgångsrik, en inte.

Ett åberopar lås B åberopar lås A får ett "misslyckat" svar B får "lyckat" svar

En sekventiell historia är en där alla anrop har omedelbara svar; det är anropet och svaret anses ske omedelbart. En sekventiell historia borde vara trivial att resonera kring, eftersom den inte har någon verklig samtidighet; det tidigare exemplet var inte sekventiellt och är därför svårt att resonera kring. Det är här lineariserbarhet kommer in.

En historik är linjäriserbar om det finns en linjär ordning av de genomförda operationerna så att:

  1. För varje genomförd operation i returnerar operationen samma resultat i exekveringen som operationen skulle returnera om varje operation genomfördes en efter en i ordningen .
  2. Om en operation op 1 slutförs (får ett svar) innan op 2 börjar (anropar), så föregår op 1 op 2 i .

Med andra ord:

  • dess anrop och svar kan ordnas om för att ge en sekventiell historia;
  • att sekventiell historia är korrekt enligt den sekventiella definitionen av objektet;
  • om ett svar föregick ett anrop i den ursprungliga historien, måste det fortfarande föregå det i den sekventiella omordningen.

(Observera att de två första punkterna här matchar serialiserbarhet : operationerna verkar ske i någon ordning. Det är den sista punkten som är unik för lineariserbarhet och är således det största bidraget från Herlihy och Wing.)

Låt oss titta på två sätt att ändra ordning på låsexemplet ovan.

Ett åberopar lås A får ett "misslyckat" svar B åberopar lås B får "lyckat" svar

Omordning av B:s anrop under A:s svar ger en sekventiell historia. Detta är lätt att resonera kring, eftersom alla operationer nu sker i en uppenbar ordning. Tyvärr stämmer det inte överens med objektets sekventiella definition (det stämmer inte överens med programmets semantik): A borde ha lyckats erhålla låset, och B skulle därefter ha avbrutit.

B åberopar lås B får "lyckat" svar Ett åberopar lås A får ett "misslyckat" svar

Detta är en annan korrekt sekventiell historia. Det är också en linjärisering! Observera att definitionen av lineariserbarhet endast utesluter att svar som föregår anrop kan ordnas om; eftersom den ursprungliga historien inte hade några svar före anrop, kan vi ordna om den som vi vill. Därför är den ursprungliga historien verkligen linjäriserbar.

Ett objekt (i motsats till en historia) är lineariserbart om alla giltiga historiker för dess användning kan linjäriseras. Observera att detta är ett mycket svårare påstående att bevisa.

Lineariserbarhet kontra serialiserbarhet

Tänk på följande historia, återigen om två objekt som interagerar med ett lås:

Ett åberopar lås A låser framgångsrikt B anropar upplåsning B låser upp A åberopar upplåsning A låses upp

Denna historia är inte giltig eftersom det finns en punkt där både A och B håller låset; dessutom kan den inte omordnas till en giltig sekventiell historik utan att bryta mot ordningsregeln. Därför är den inte lineariserbar. Men under serialisering kan B:s upplåsningsoperation flyttas till före A:s ursprungliga lås, vilket är en giltig historik (förutsatt att objektet börjar historiken i ett låst tillstånd):

B anropar upplåsning B låser upp Ett åberopar lås A låser framgångsrikt A åberopar upplåsning A låses upp

Denna omordning är förnuftig förutsatt att det inte finns något alternativt sätt att kommunicera mellan A och B. Linjäriserbarhet är bättre när man betraktar enskilda objekt separat, eftersom omordningsbegränsningarna säkerställer att flera linjäriserbara objekt, betraktade som en helhet, fortfarande är linjäriserbara.

Linjäriseringspunkter

Denna definition av lineariserbarhet är ekvivalent med följande:

  • Alla funktionsanrop har en linjäriseringspunkt vid något ögonblick mellan deras anrop och deras svar.
  • Alla funktioner verkar uppträda omedelbart vid sin linjäriseringspunkt och beter sig som specificerats av den sekventiella definitionen.

Detta alternativ är vanligtvis mycket lättare att bevisa. Det är också mycket lättare att resonera kring som användare, mycket på grund av dess intuitivitet. Denna egenskap att inträffa momentant, eller odelbart, leder till användningen av termen atomär som ett alternativ till det längre "lineariserbara".

I exemplen nedan är linjäriseringspunkten för räknaren byggd på compare-and-swap linjäriseringspunkten för den första (och enda) framgångsrika compare-and-swap-uppdateringen. Räknaren som byggts med låsning kan anses linjäriseras när som helst medan låsen hålls, eftersom alla potentiellt motstridiga operationer är uteslutna från att köras under den perioden.

Primitiva atominstruktioner

[ relevant? ]

Processorer har instruktioner som kan användas för att implementera låsning och låsfria och väntefria algoritmer . Möjligheten att tillfälligt hämma avbrott , vilket säkerställer att den för närvarande pågående processen inte kan kontextväxlas , räcker också på en enprocessor . Dessa instruktioner används direkt av kompilatorer och skrivare av operativsystem men är också abstraherade och exponerade som bytekoder och biblioteksfunktioner på språk på högre nivå:

De flesta [ citat behövs ] -processorer inkluderar butiksoperationer som inte är atomära med avseende på minne. Dessa inkluderar flerordslager och strängoperationer. Om ett avbrott med hög prioritet inträffar när en del av butiken är klar måste operationen slutföras när avbrottsnivån återställs. Rutinen som behandlar avbrottet får inte modifiera minnet som ändras. Det är viktigt att ta hänsyn till detta när man skriver avbrottsrutiner.

När det finns flera instruktioner som måste slutföras utan avbrott, används en CPU-instruktion som tillfälligt inaktiverar avbrott. Detta måste hållas till endast ett fåtal instruktioner och avbrotten måste återaktiveras för att undvika oacceptabel svarstid på avbrott eller till och med förlorade avbrott. Denna mekanism är inte tillräcklig i en miljö med flera processorer eftersom varje CPU kan störa processen oavsett om avbrott inträffar eller inte. Vidare, i närvaro av en instruktionspipeline , utgör avbrottsfria operationer en säkerhetsrisk, eftersom de potentiellt kan kedjas i en oändlig loop för att skapa en överbelastningsattack , som i Cyrix-koma-buggen .

C -standarden och SUSv3 ger sig_atomic_t för enkla atomära läsningar och skrivningar; att öka eller minska är inte garanterat atomärt. Mer komplexa atomoperationer finns i C11 , vilket ger stdatomic.h . Kompilatorer använder hårdvarufunktionerna eller mer komplexa metoder för att implementera operationerna; ett exempel är libatomic av GCC.

ARM -instruktionsuppsättningen tillhandahåller LDREX- och STREX -instruktioner som kan användas för att implementera atomminnesåtkomst genom att använda exklusiva monitorer implementerade i processorn för att spåra minnesåtkomster för en specifik adress. Men om en kontextväxling inträffar mellan samtal till LDREX och STREX , noterar dokumentationen att STREX kommer att misslyckas, vilket indikerar att operationen bör försökas igen.

Atomverksamhet på hög nivå

Det enklaste sättet att uppnå linjäriserbarhet är att köra grupper av primitiva operationer i en kritisk sektion . Strängt sett kan oberoende operationer sedan noggrant tillåtas att överlappa sina kritiska sektioner, förutsatt att detta inte bryter mot lineariserbarheten. Ett sådant tillvägagångssätt måste balansera kostnaden för ett stort antal lås mot fördelarna med ökad parallellitet.

Ett annat tillvägagångssätt, som gynnas av forskare (men som ännu inte används i stor utsträckning i mjukvaruindustrin), är att designa ett linjäriserbart objekt med hjälp av de ursprungliga atomära primitiv som tillhandahålls av hårdvaran. Detta har potential att maximera tillgänglig parallellitet och minimera synkroniseringskostnader, men kräver matematiska bevis som visar att objekten beter sig korrekt.

En lovande hybrid av dessa två är att tillhandahålla en transaktionsminnesabstraktion . Som med kritiska avsnitt markerar användaren sekventiell kod som måste köras isolerat från andra trådar. Implementeringen säkerställer sedan att koden exekveras atomiskt. Denna abstraktionsstil är vanlig när man interagerar med databaser; till exempel, när du använder Spring Framework , kommer annotering av en metod med @Transactional att säkerställa att alla slutna databasinteraktioner sker i en enda databastransaktion . Transaktionsminnet går ett steg längre och säkerställer att alla minnesinteraktioner sker atomärt. Precis som med databastransaktioner uppstår frågor om sammansättningen av transaktioner, särskilt databas- och in-memory-transaktioner.

Ett vanligt tema när man designar linjäriserbara objekt är att tillhandahålla ett allt-eller-inget-gränssnitt: antingen lyckas en operation helt eller så misslyckas den och gör ingenting. ( ACID- databaser hänvisar till denna princip som atomicitet .) Om operationen misslyckas (vanligtvis på grund av samtidiga operationer), måste användaren försöka igen, vanligtvis utföra en annan operation. Till exempel:

  • Compare-and-swap skriver ett nytt värde till en plats endast om den senares innehåll matchar ett angett gammalt värde. Detta används vanligtvis i en läs-modifiera-CAS-sekvens: användaren läser platsen, beräknar ett nytt värde att skriva och skriver det med ett CAS (jämför-och-byt); om värdet ändras samtidigt kommer CAS att misslyckas och användaren försöker igen.
  • Load-link/store-conditional kodar detta mönster mer direkt: användaren läser platsen med load-link, beräknar ett nytt värde att skriva och skriver det med store-conditional; om värdet har ändrats samtidigt, kommer SC (store-conditional) att misslyckas och användaren försöker igen.
  • I en databastransaktion , om transaktionen inte kan slutföras på grund av en samtidig operation (t.ex. i ett dödläge ), kommer transaktionen att avbrytas och användaren måste försöka igen.

Exempel på linjäriserbarhet

Räknare

För att demonstrera kraften och nödvändigheten av lineariserbarhet kommer vi att överväga en enkel räknare som olika processer kan öka.

Vi skulle vilja implementera ett motobjekt som flera processer kan komma åt. Många vanliga system använder sig av räknare för att hålla reda på hur många gånger en händelse har inträffat.

Räknarobjektet kan nås av flera processer och har två tillgängliga operationer.

  1. Öka - lägger till 1 till värdet som är lagrat i räknaren, returkvittering
  2. Läs - returnerar det aktuella värdet som är lagrat i räknaren utan att ändra det.

Vi kommer att försöka implementera detta motobjekt med hjälp av delade register

Vårt första försök som vi kommer att se är icke-lineariserbart har följande implementering med ett delat register bland processerna.

Icke-atomär

Den naiva, icke-atomära implementeringen:

Ökning:

  1. Läs av värdet i registret R
  2. Lägg till en till värdet
  3. Skriver tillbaka det nya värdet i register R

Läsa:

Läs register R

Denna enkla implementering är inte linjäriserbar, vilket visas av följande exempel.

Föreställ dig att två processer körs för åtkomst till det enda räknarobjektet som initierats till att ha värdet 0:

  1. Den första processen läser värdet i registret som 0.
  2. Den första processen lägger till ett till värdet, räknarens värde bör vara 1, men innan den har skrivit klart det nya värdet tillbaka till registret kan det bli avstängt, medan den andra processen körs:
  3. Den andra processen läser värdet i registret, vilket fortfarande är lika med 0;
  4. Den andra processen lägger till en till värdet;
  5. den andra processen skriver in det nya värdet i registret, registret har nu värdet 1.

Den andra processen är klar och den första processen fortsätter att köras där den slutade:

  1. Den första processen skriver 1 i registret, omedveten om att den andra processen redan har uppdaterat värdet i registret till 1.

I exemplet ovan anropade två processer ett inkrementkommando, men värdet på objektet ökade bara från 0 till 1, istället för 2 som det borde ha. En av inkrementoperationerna gick förlorad till följd av att systemet inte kunde linjäriseras.

Ovanstående exempel visar behovet av att noggrant tänka igenom implementeringar av datastrukturer och hur lineariserbarhet kan påverka systemets korrekthet.

Atom

För att implementera ett linjäriserbart eller atomiskt motobjekt kommer vi att modifiera vår tidigare implementering så att varje process P i kommer att använda sitt eget register R i

Varje process ökar och läser enligt följande algoritm:

Ökning:

  1. Avläst värde i register R i .
  2. Lägg till en till värdet.
  3. Skriv tillbaka ett nytt värde i R i

Läsa:

  1. Läs register R 1, R 2, ... R n .
  2. Returnera summan av alla register.

Denna implementering löser problemet med vår ursprungliga implementering. I detta system linjäriseras inkrementoperationerna vid skrivsteget. Linjäriseringspunkten för en inkrementoperation är när den operationen skriver det nya värdet i sitt register R i. Läsoperationerna linjäriseras till en punkt i systemet när värdet som returneras av läsningen är lika med summan av alla värden lagrade i varje register Ri .

Detta är ett trivialt exempel. I ett riktigt system kan operationerna vara mer komplexa och de fel som introduceras extremt subtila. Till exempel kan läsning av ett 64-bitars värde från minnet faktiskt implementeras som två sekventiella läsningar av två 32-bitars minnesplatser. Om en process bara har läst de första 32 bitarna, och innan den läser de andra 32 bitarna ändras värdet i minnet, kommer den att ha varken det ursprungliga värdet eller det nya värdet utan ett blandat värde.

Dessutom kan den specifika ordningen i vilken processerna körs förändra resultaten, vilket gör ett sådant fel svårt att upptäcka, reproducera och felsöka .

Jämför-och-byt

Huvudartikel: Jämför-och-byt

De flesta system tillhandahåller en atomic compare-and-swap-instruktion som läser från en minnesplats, jämför värdet med ett "förväntat" tillhandahållet av användaren och skriver ut ett "nytt" värde om de två matchar, vilket returnerar om uppdateringen lyckades . Vi kan använda detta för att fixa den icke-atomära räknaralgoritmen enligt följande:

  1. Läs värdet i minnesplatsen;
  2. lägg till en till värdet;
  3. använd compare-and-swap för att skriva tillbaka det inkrementerade värdet;
  4. Försök igen om värdet som lästs in av compare-and-swap inte matchade värdet vi ursprungligen läste.

Eftersom jämför-och-bytet inträffar (eller verkar inträffa) omedelbart, om en annan process uppdaterar platsen medan vi pågår, kommer jämför-och-bytet garanterat att misslyckas.

Hämta-och-öka

Huvudartikel: Hämta-och-öka

Många system tillhandahåller en atomär hämta-och-ökningsinstruktion som läser från en minnesplats, villkorslöst skriver ett nytt värde (det gamla värdet plus ett) och returnerar det gamla värdet. Vi kan använda detta för att fixa den icke-atomära räknaralgoritmen enligt följande:

  1. Använd hämta-och-öka för att läsa det gamla värdet och skriv tillbaka det inkrementerade värdet.

Att använda hämta-och-öka är alltid bättre (kräver färre minnesreferenser) för vissa algoritmer – som den som visas här – än jämför-och-byt, även om Herlihy tidigare bevisat att jämför-och-byt är bättre för vissa andra algoritmer som kan inte implementeras alls med enbart hämta-och-öka. Så CPU-designer med både hämta-och-öka och jämför-och-byta (eller motsvarande instruktioner) kan vara ett bättre val än sådana med bara det ena eller det andra.

Låsning

Huvudartikel: Lock (datavetenskap)

Ett annat tillvägagångssätt är att förvandla den naiva algoritmen till en kritisk sektion , förhindra att andra trådar stör den, med hjälp av ett lås . Återigen fixar den icke-atomära räknaralgoritmen:

  1. Skaffa ett lås, utesluta andra trådar från att köra den kritiska delen (steg 2–4) samtidigt;
  2. läs värdet i minnesplatsen;
  3. lägg till en till värdet;
  4. skriv det inkrementerade värdet tillbaka till minnesplatsen;
  5. släpp låset.

Denna strategi fungerar som förväntat; låset hindrar andra trådar från att uppdatera värdet tills det släpps. Jämfört med direkt användning av atomära operationer kan det emellertid drabbas av betydande overhead på grund av låskonflikter. För att förbättra programmets prestanda kan det därför vara en bra idé att ersätta enkla kritiska sektioner med atomoperationer för icke-blockerande synkronisering (som vi just har gjort för räknaren med jämför-och-byta och hämta-och-öka), istället för tvärtom, men tyvärr är en betydande förbättring inte garanterad och låsfria algoritmer kan lätt bli för komplicerade för att vara värda mödan.

Se även

Vidare läsning

Hämtad från " https://en.wikipedia.org/w/index.php?title=Linearizability&oldid=1134247779 "