Separační logika

Separační logika , separační logika ( angl . separační logika ) - formální systém, substrukturální logika, použitelné pro ověřování programů obsahujících proměnlivé datové struktury a ukazatele , rozšíření Hoareovy logiky . Navrhli John Reynolds , Peter O'Hearn , Samin Ishtiaq a Hongseok Yang [ 1 ] [ 2 ] [ 3] [4] na základě práce Roda Burstalla [ 5 ] . Jazyk asercí rozdělovací logiky je speciálním případem logiky skupinových implikací [ 6 ] .

Evolucí logiky dělení pro paralelní výpočty se sdílenou pamětí je logika paralelního dělení vyvinutá O'Hearnem a Stephenem D. Brookesem .

Technologie založené na logice separace umožňují vyvíjet systémy pro ověřování velkých softwarových projektů [7] .

Předpoklady pro vytvoření

Hoareova logika má řadu omezení, pracuje pouze s proměnnými proměnnými a nepodporuje procedury ani kód první třídy . Největším omezením je však chybějící podpora ukazatelů , která je pro imperativní specifikaci programu nejrelevantnější . V případě použití ukazatelů a haldy lze proměnlivé proměnné opustit tím , že místním proměnným přiřadíme hodnotu ukazatele pouze jednou [8] .

V letech 2000-2002 přišli John Reynolds a Peter O'Hearn s rozšířením Hoareovy logiky, logikou dělení. Původní myšlenkou bylo zjednodušit uvažování o nízkoúrovňových imperativních programech s běžnou proměnlivou datovou strukturou [9] . Samotný termín je spojen s hlavní myšlenkou této logiky - popisem rozdělení úložiště ( anglicky storage ) na nepřekrývající se komponenty. Termín se používá jak ve vztahu k predikátovému počtu rozšířenému operátorem dělení , tak k výsledku rozšíření Hoareovy logiky [1] .

Popis

Klíčovým rysem logiky separace je možnost lokálního uvažování (lokálního uvažování) díky přítomnosti ve výpovědích prostorových spojek ( angl. prostorových spojek ) mezi částmi haldy [10] .

Logika vám umožňuje pracovat s příkazy formuláře , kde: $s,h\models P$

$s$ - paměť (například ve formě zásobníku [1] ), konečné částečné funkční zobrazení z proměnných na celá čísla ,
$h$ je halda, konečné částečné funkční mapování z celých čísel na celá, a
$P$ - výpis o paměti a haldě, tedy o stavu programu [12] .

K překonání těžkopádných popisů zákazů používání stejné adresy různými objekty byla zavedena nová logická operace - disjunktní spojka , označená (nebo [13] ) a tvrdící, že každá z podmínek a jsou splněny ve svém část haldy (adresné úložiště ) [9] [14] . To platí pro hromadu , pokud existují dvě části této hromady a pro kterou platí [15] : $P\ *\ Q$ $P\ \land \!*\ Q$ $P$ $Q$ $P\ *\ Q$ $h$ $h_1$ $h_2$

Regiony a se neprotínají; $h_1$ $h_2$
$h$ je spojení a ; $h_1$ $h_2$
$P$ true pro všechny adresy od ; $h_1$
$Q$ platí pro všechny adresy od . $h_2$

Výše a jsou chápány jako dílčí funkce , které dávají hodnoty odpovídající adrese na haldě. $h_1$ $h_2$

Aby se potvrdilo, že halda je prázdná, zavede se predikát (v tomto případě samozřejmě ) a pro označení ukazatele - . Například v následujícím, což je jeden z axiomů, Hoareova trojice $emp$ $P\ *\ emp\ \Leftrightarrow \ P$ $e\mapsto x$

{\displaystyle \{E\mapsto -\}\ [E]:=F\ \{E\mapsto F\))

předpokladem je nevyužitá paměťová buňka, která v důsledku operace přiřazení ukazuje na F , což je uvedeno v postpodmínce [12] .

Klíčem k místnímu uvažování je rámcové pravidlo zavedené O'Hearnem [ 1 ] :

\frac{\{P\}\ C\ \{Q\}}{\{P \ast R\}\ C\ \{Q \ast R\}}~\mathsf{mod}(C) \cap \ mathsf{fv}(R) =\emptyset

ve kterém není pod vlivem příkazu změněna žádná volná proměnná ( angl . free proměnná ) . Pomocí tohoto pravidla můžete přidat libovolné predikáty o proměnných a částech haldy, které nejsou modifikovány příkazem . Zároveň O'Hearn nazval množství hromady obsazené příkazem termínem angličtina. stopa („otisk“). Účelem rámcového pravidla je rozšířit argument z lokálnějšího popisu příkazu na globálnější popis obklopujícího příkazu, příkazu s největším potiskem [1] . $R$ $C$ $C$

Poté, co Yang a Ishtiak zjistili, že logika separace je příkladem logiky svazkových implikací, zavedli separační implikaci ( anglicky separating implication [1] , anglicky magic wand ). Označení říká, že pokud byla halda rozšířena o neprotínající se haldu, pro kterou je true , pak pro výslednou haldu to bude pravda [7] . $P-\!\!\!\ast\, Q$ $P$ $Q$

Sémantika logických spojek (oddělovací konjunkce a oddělovací implikace) implikuje monoidní haldovou strukturu [7] .

Parallel Separation Logic (CSL)

Concurrent Separation Logic ( CSL ) je verze logiky použitelná pro ověřování paralelních algoritmů se sdílenou pamětí. Původně navrhl Peter O'Hearn. Používá následující pravidlo [16]

{\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\)) {\{P_{1}*P_{2}\}\;C_{1}\paralelní C_{2}\;\{Q_{1}*Q_{2}\))))

což vám umožňuje vyvozovat závěry za přítomnosti nezávislých vláken provádění přistupujících k samostatnému úložišti. O'Hearnova pravidla důkazu přizpůsobila raný přístup Tonyho Hoareho k souběžnosti [17] tím, že nahradila použití omezení rozsahu k vynucení rozdělování uvažováním v logice rozdělování. Kromě rozšíření Hoareho přístupu k ukazatelům haldy O'Hearn ukázal, že logika paralelního dělení může dynamicky sledovat přenos vlastnictví oblastí haldy mezi procesy. Příklady v jeho článku tedy zahrnují vyrovnávací paměť pro ukazatel a správce paměti .

Místní uvažování lze chápat i z hlediska převodu vlastnictví . Nejjednodušší je uvažovat jako příklad o převodu vlastnictví pomocí pravidel monitoru Hoare (můžete vidět, že logika oddělení je vhodná i pro distribuované systémy). Pro zadání kritické sekce se používá oddělovací spojka s , kde je invariant zdroje r . Po opuštění kritické sekce následuje logický závěr v opačném směru [18] : $Ir$ $Ir$

\frac{\{P \ast I_r\}\ C\ \{Q \ast I_r\}}{\{P\}\ \mathsf{with}\ r\ \mathsf{do}\ C\ \{Q\ }}

Analogicky můžeme uvažovat i o procesu zpracování zprávy procesem odeslané jiným procesem se zdroji delegovanými na tento proces, určenými otisky prstů [18] .

Model pro paralelní rozdělovací logiku poprvé představil Stephen D. Brookes v doprovodném článku k O'Hearnovu článku [19] . Správnost ( anglicky soundness ) logiky byla obtížným problémem. Konkrétně protipříklad Johna Reynoldse ukázal selhání dřívější, nepublikované verze logiky. Pointa vznesená Reynoldsovým příkladem je stručně popsána v O'Hearnově článku a úplněji v Brooksově článku.

O'Hearn a Brooks jsou spolupříjemci Gödelovy ceny za rok 2016 za vynález logiky paralelního dělení [20] .

Aplikace a implementace

Logika oddělení našla uplatnění v automatických a interaktivních ověřovačích softwaru napsaného imperativním a objektově orientovaným stylem. Za tímto účelem byly vyvinuty vhodné doplňky stávajících ověřovacích nástrojů, například:

Ynot [21] je knihovna pro ověřování imperativních programů pro Coq .
Predator [22] je programový analyzátor založený na rozdělené logice pro analýzu programů obsahujících dynamické seznamy [23] .

Další systémy využívající rozdělenou logiku: Smallfoot, Space Invader, THOR, SLAyer, HIP, jStar, Xisa, VeriFast, Infer, SeLoger, SLP. Od roku 2014 však neexistují žádné praktické důkazy teorémů, které by implementovaly plnou logiku dělení, tj. včetně implikace dělení [7] .

Podle charakteru použití systému jej lze rozdělit následovně [24] :

Uživatel ručně zapisuje specifikaci i důkaz pomocí taktiky: interaktivní teorémové důkazy Coq, HOL4, Isabelle/HOL.
Uživatel zapíše specifikaci a invarianty smyčky : nezávislé ověřovací nástroje Smallfoot, HIP, Verifast, Jstar.
Uživatel zapíše pouze specifikaci (nebo dokonce nic nenapíše): nástroje pro analýzu tvaru ( angl . shape analysis ) Space Invader, THOR, Xisa, SLAyer.

Poznámky

↑ 1 2 3 4 5 6 Reynolds, 2002 .
↑ Intuicionistické uvažování o sdílené proměnlivé datové struktuře. John Reynolds. Millennial Perspectives in Computer Science, sborník z Oxford-Microsoft Symposium v roce 1999 na počest sira Tonyho Hoara
↑ BI jako asertion Language pro měnitelné datové struktury. Samin Ishtiaq, Peter O'Hearn. POPL 2001.
↑ Místní zdůvodnění o programech, které mění datové struktury. Archivováno 27. září 2013 na Wayback Machine Peter O'Hearn, John Reynolds, Hongseok Yang . CSL 2001
↑ Některé techniky pro dokazování programů, které mění datové struktury. RM Burstall. Strojová inteligence 7, 1972.
↑ The Logic of Bunched Implications PW O'Hearn a DJ Pym. Bulletin of Symbolic Logic, 5(2), červen 1999, str. 215-244
↑ 1 2 3 4 Lee, Park, 2014 .
↑ Programy a důkazy, 2014 .
↑ 12 Reynolds , 2008 .
↑ Parkinson, Bierman, 2005 .
↑ Chris Poskitt Software Verification (podzim 2013) Přednáška 5: Separation Logic Parts I - II (downlink)
↑ 1 2 A Primer on Separation Logic, 2012 .
↑ Tjark Weber (2004). „Směrem k mechanizovanému ověřování programu se separační logikou“. Computer Science Logic~-- 18. mezinárodní workshop, CSL 2004, 13. výroční konference EACSL, Karpacz, Polsko, září 2004, sborník příspěvků . Poznámky z přednášek z informatiky. Springer. str. 250-264. weber04 směrem k . Staženo 2013-12-06 . |access-date=vyžaduje |url=( pomoc )
↑ Matthew J. Parkinson Místní zdůvodnění pro Javu Archivováno 23. září 2015 na Wayback Machine , 2005, UCAM-CL-TR-654, ISSN 1476-2986
↑ Přednáška 24: Analýza ukazatelů a tvaru Archivováno 29. listopadu 2014 na Wayback Machine , LARA, EPFL
↑ O'Hearn, Peter (2007). „Zdroje, souběžnost a místní uvažování“ (PDF) . Teoretická informatika . 375 (1-3): 271-307. DOI : 10.1016/j.tcs.2006.12.035 . Archivováno (PDF) z originálu dne 2021-03-04 . Získáno 24. 3. 2021 . Použitý zastaralý parametr |deadlink=( nápověda )
↑ Hoare, CAR (1972). „Směrem k teorii paralelního programování“. Techniky operačního systému. Academic Press .
↑ 1 2 Étienne Lozes Information as Resource in Separation Logic (unavailable link) , ANR project, draft
↑ Brookes, Stephen (2007). „Sémantika pro souběžnou separační logiku“ (PDF) . Teoretická informatika . 375 (1-3): 227-270. DOI : 10.1016/j.tcs.2006.12.034 . Archivováno (PDF) z originálu dne 2021-05-09 . Získáno 24. 3. 2021 . Použitý zastaralý parametr |deadlink=( nápověda )
↑ European Association for Theoretical Computer Science 2016 Gödel Prize Archivováno 14. července 2016 na Wayback Machine
↑ Ano . Získáno 19. listopadu 2014. Archivováno z originálu 25. února 2009. (neurčitý)
↑ Predátoři . Datum přístupu: 19. listopadu 2014. Archivováno z originálu 25. října 2014. (neurčitý)
↑ Mutilin V.S., Novikov E.M., Khoroshilov A.V. Přehled nástrojů pro statickou verifikaci programů C aplikovaných na ovladače zařízení operačního systému Linux // Sborník Institutu pro systémové programování Ruské akademie věd. - 2012. - T. 22 , č. 3 . - S. 293-326 .
↑ Cliff Jones (z U. Newcastle), Viktor Vafeiadis (z MPI-SWS) Rely-garante myšlení a separační logika Archivováno 29. listopadu 2014 na Wayback Machine

Literatura

Reynolds J. C. Separation Logic: A Logic for Shared Mutable Data Structures // LICS '02 :of the 17th Annual IEEE Symposium on Logic in Computer Science - Washington, DC, USA : IEEE Computer Society , 2002. - S. 55-74. - ISBN 978-0-7695-1483-3 - doi:10.1109/LICS.2002.1029817
Reynolds J. C. An Overview of Separation Logic // Verified Software : Theories, Tools, Experiments : First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Curych, Switzerland, October 10-13, 2005, Revidované vybrané články a diskuse / B. Meyer , J. Woodcock - Berlin : Springer Berlin Heidelberg , 2008. - S. 460-469. - ( Lecture Notes in Computer Science ; Vol. 4171) - ISBN 978-3-540-69147-1 - ISSN 0302-9743 ; 1611-3349 – doi:10.1007/978-3-540-69149-5_49
Parkinson M. , Bierman G. Separation Logic and Abstraction (anglicky) // POPL '05 : Sborník z 32. sympozia ACM SIGPLAN-SIGACT o principech programovacích jazyků Long Beach, CA, USA 12.–14. ledna 2005 — Nové York, NY, USA : ACM , 2005. - S. 247-258. - ISBN 978-1-58113-830-6 - doi:10.1145/1040305.1040326
Lee, Wonyeol a Park, Sungwoo. A Proof System for Separation Logic with Magic Wand (anglicky) // SIGPLAN Not .. - ACM, 2014. - Vol. 49 , č. 1 . - str. 477--490 . — ISSN 0362-1340 .
Appel A. , Dockins R. , Hobor A. , Beringer L. , Dodds J. , Blazy S. , Leroy X. Program Logics for Certified Compilers (anglicky) - Cambridge University Press , 2014. - 472 s. — ISBN 978-1-107-04801-0
Ilja Sergej. 8.2 Základy separační logiky // Programy a důkazy: Mechanizace matematiky se závislými typy . - 2014. - (Poznámky z přednášky).
Peter W. O'Hearn. A Primer on Separation Logic (a automatické ověřování a analýza programu) // Bezpečnost a zabezpečení softwaru; Nástroje pro analýzu a ověřování. - 2012. - Sv. 33. - S. 286-318.

Odkazy

Cliff Jones ( Newcastle University ), Viktor Vafeiadis ( MPI-SWS ) Rely-garante thinking & separation logic (ang.) - prezentace dobře ilustrující koncepty separační logiky
Matthew Parkinson Úvod do separační logiky (anglicky) - prezentace, ve které jsou ilustrovány všechny hlavní aspekty separační logiky: axiomy, příklady programů s odpovídajícími diagramy, syntaxe