Samtidighet (datavetenskap)

"Dining Philosophers" , ett klassiskt problem som involverar samtidighet och delade resurser

Inom datavetenskap är samtidighet förmågan hos olika delar eller enheter i ett program , en algoritm eller ett problem att utföras ur funktion eller i partiell ordning , utan att det påverkar resultatet. Detta möjliggör parallell exekvering av de samtidiga enheterna, vilket avsevärt kan förbättra den totala exekveringshastigheten i system med flera processorer och flera kärnor . I mer tekniska termer hänvisar samtidighet till nedbrytbarheten av ett program, en algoritm eller ett problem i ordningsoberoende eller partiellt ordnade komponenter eller beräkningsenheter.

Enligt Rob Pike är samtidighet sammansättningen av oberoende exekverande beräkningar, och samtidighet är inte parallellism: samtidighet handlar om att hantera många saker samtidigt men parallellism handlar om att göra många saker samtidigt. Samtidighet handlar om struktur, parallellism handlar om utförande, samtidighet ger ett sätt att strukturera en lösning för att lösa ett problem som kan (men inte nödvändigtvis) är parallelliserbart.

Ett antal matematiska modeller har utvecklats för generella samtidiga beräkningar, inklusive Petrinet , processkalkyler , den parallella slumpmässiga maskinmodellen , aktörsmodellen och Reo Coordination Language .

Historia

Som Leslie Lamport (2015) noterar: "Medan samtidig programexekvering hade övervägts i flera år, började datavetenskapen om samtidighet med Edsger Dijkstras framstående artikel från 1965 som introducerade problemet med ömsesidig uteslutning . ... De efterföljande decennierna har sett en enorm ett ökat intresse för samtidighet – särskilt i distribuerade system . När man ser tillbaka på fältets ursprung, är det som sticker ut den grundläggande roll som Edsger Dijkstra spelar”.

frågor

Eftersom beräkningar i ett samtidigt system kan interagera med varandra medan de exekveras, kan antalet möjliga exekveringsvägar i systemet vara extremt stort, och det resulterande resultatet kan vara obestämt . Samtidig användning av delade resurser kan vara en källa till obestämdhet som leder till problem som dödlägen och resurssvält .

Design av samtidiga system innebär ofta att man hittar tillförlitliga tekniker för att koordinera deras exekvering, datautbyte, minnesallokering och exekveringsplanering för att minimera svarstiden och maximera genomströmningen .

Teori

Samtidighetsteori har varit ett aktivt forskningsfält inom teoretisk datavetenskap . Ett av de första förslagen var Carl Adam Petris framstående arbete om Petri-nät i början av 1960-talet. Under åren sedan dess har en mängd olika formalismer utvecklats för modellering och resonemang om samtidighet.

Modeller

Ett antal formalismer för att modellera och förstå samtidiga system har utvecklats, inklusive:

Vissa av dessa modeller för samtidighet är i första hand avsedda att stödja resonemang och specifikation, medan andra kan användas genom hela utvecklingscykeln, inklusive design, implementering, bevis, testning och simulering av samtidiga system. Vissa av dessa är baserade på meddelandeöverföring , medan andra har olika mekanismer för samtidighet.

Spridningen av olika modeller av samtidighet har motiverat vissa forskare att utveckla sätt att förena dessa olika teoretiska modeller. Till exempel har Lee och Sangiovanni-Vincentelli visat att en så kallad "taggad-signal"-modell kan användas för att tillhandahålla ett gemensamt ramverk för att definiera denotationssemantiken för en mängd olika modeller av samtidighet, medan Nielsen, Sassone och Winskel har visat att kategoriteori kan användas för att ge en liknande enhetlig förståelse av olika modeller.

Concurrency Representation Theorem i aktörsmodellen ger ett ganska generellt sätt att representera samtidiga system som är stängda i den meningen att de inte tar emot kommunikation utifrån. (Andra samtidighetssystem, t.ex. processkalkyler kan modelleras i aktörsmodellen med hjälp av ett tvåfas commit-protokoll .) Den matematiska beteckningen som betecknas av ett slutet system S konstrueras allt bättre approximationer från ett initialt beteende som kallas S med hjälp av ett beteende approximerande funktion progression S för att konstruera en denotation (betydelse) för S enligt följande:

Beteckna S ≡ ⊔ i∈ω progression S i (⊥ S )

På så sätt kan S matematiskt karakteriseras i termer av alla dess möjliga beteenden.

Logik

Olika typer av tidslogik kan användas för att resonera kring samtidiga system. Vissa av dessa logiker, såsom linjär temporal logik och beräkningsträdlogik , tillåter påståenden att göras om sekvenserna av tillstånd som ett samtidigt system kan passera. Andra, såsom handlingsberäkningsträdlogik, Hennessy–Milner-logik och Lamports temporala handlingslogik , bygger sina påståenden från sekvenser av åtgärder (tillståndsförändringar). Den huvudsakliga tillämpningen av dessa logiker är att skriva specifikationer för samtidiga system.

Öva

Samtidig programmering omfattar programmeringsspråk och algoritmer som används för att implementera samtidiga system. Samtidig programmering anses vanligtvis vara mer generell än parallell programmering eftersom den kan involvera godtyckliga och dynamiska mönster av kommunikation och interaktion, medan parallella system i allmänhet har ett fördefinierat och välstrukturerat kommunikationsmönster. Grundmålen för samtidig programmering inkluderar korrekthet , prestanda och robusthet . Samtidiga system som operativsystem och databashanteringssystem är i allmänhet utformade för att fungera på obestämd tid, inklusive automatisk återställning från fel, och inte avslutas oväntat (se Samtidighetskontroll ) . Vissa samtidiga system implementerar en form av transparent samtidighet, där samtidiga beräkningsenheter kan konkurrera om och dela en enda resurs, men komplexiteten i denna konkurrens och delning är skyddad från programmeraren.

Eftersom de använder delade resurser kräver samtidiga system i allmänhet inkludering av någon form av arbiter någonstans i deras implementering (ofta i den underliggande hårdvaran), för att kontrollera åtkomsten till dessa resurser. Användningen av arbiters introducerar möjligheten till obestämdhet vid samtidig beräkning, vilket har stora konsekvenser för praktiken inklusive korrekthet och prestanda. Till exempel introducerar skiljedom obunden obestämdhet som väcker problem med modellkontroll eftersom det orsakar explosioner i tillståndsutrymmet och kan till och med få modeller att ha ett oändligt antal tillstånd.

Vissa modeller för samtidig programmering inkluderar samprocesser och deterministisk samtidighet . I dessa modeller ger kontrolltrådar uttryckligen sina tidsintervall, antingen till systemet eller till en annan process.

Se även

Vidare läsning

externa länkar