Separationslogik

Separationslogik , separationslogik ( engelsk separationslogik ) - formellt system, substrukturell logik, tillämplig på verifiering av program som innehåller föränderliga datastrukturer och pekare , en förlängning av Hoares logik . Designad av John Reynolds , Peter O'Hearn , Samin Ishtiaq och Hongseok Yang [ 1 ] [ 2 ] [ 3 ] [4] baserat på arbetet av Rod Burstall [ 5 ] . Påståendespråket för partitioneringslogik är ett specialfall av logiken med samlade implikationer [ 6 ] .

En utveckling av partitioneringslogik för parallell beräkning med delat minne är parallell partitioneringslogik , utvecklad av O'Hearn och Stephen D. Brookes .

Teknik baserad på separationslogiken gör det möjligt att utveckla system för verifiering av stora programvaruprojekt [7] .

Förutsättningar för att skapa

Hoares logik har ett antal begränsningar, den fungerar bara på föränderliga variabler och inte stöder procedurer eller förstklassig kod . Den största begränsningen är dock bristen på pekarstöd , vilket är mest relevant för Imperative Program Specification . I fallet med att använda pekare och heap , kan föränderliga variabler överges genom att tilldela ett pekarvärde till lokala variabler endast en gång [8] .

2000-2002 kom John Reynolds och Peter O'Hearn på en förlängning av Hoares logik, divisionslogiken. Den ursprungliga idén var att förenkla resonemang om imperativa program på låg nivå med en gemensam föränderlig datastruktur [9] . Termen i sig är förknippad med huvudidén i denna logik - beskrivningen av uppdelningen av lagring ( engelsk lagring ) i icke-överlappande komponenter. Termen används både i förhållande till predikatkalkylen , utökad med divisionsoperatorn , och till resultatet av en förlängning av Hoares logik [1] .

Beskrivning

Ett nyckeldrag i separationslogiken är möjligheten till lokalt resonemang (lokalt resonemang) på grund av förekomsten i uttalandena av spatial connectives ( eng. spatial connectives ) mellan delar av högen [10] .

Logik låter dig arbeta med påståenden i formen , där: $s,h\models P$

$s$ - minne (till exempel i form av en stack [1] ), en ändlig partiell funktionell mappning från variabler till heltal ,
$h$ är en hög, en finit partiell funktionell mappning från heltal till heltal, och
$P$ - ett uttalande om minne och heap, det vill säga om programmets tillstånd [12] .

För att övervinna de besvärliga beskrivningarna av förbud mot användning av samma adress av olika objekt, har en ny logisk operation införts - en disjunkt konjunktion , betecknad med (eller [13] ) och hävdar att vart och ett av villkoren och är uppfyllda i dess del av högen (adresserat lager ) [9] [14] . Det vill säga sant för en hög om det finns två delar av denna hög och för vilken [15] är sant : $P\ *\ Q$ $P\ \land \!*\ Q$ $P$ $F$ $P\ *\ Q$ $h$ $h_1$ $h_2$

Regionerna och skär inte; $h_1$ $h_2$
$h$ är föreningen av och ; $h_1$ $h_2$
$P$ sant för alla adresser från ; $h_1$
$F$ sant för alla adresser från . $h_2$

Ovan, och förstås som delfunktioner som ger värden som motsvarar en adress på högen. $h_1$ $h_2$

För att hävda att högen är tom, introduceras ett predikat (i detta fall uppenbarligen, ), och för att beteckna en pekare - . Till exempel i det följande, som är ett av axiomen, Hoare-trippeln $emp$ $P\ *\ emp\ \Leftrightarrow \ P$ $e\mapsto x$

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

förutsättningen är den oanvända minnescellen, som, som ett resultat av tilldelningsoperationen, pekar på F , som anges i postvillkoret [12] .

Nyckeln till lokalt resonemang är ramregeln som introducerades av O'Hearn [ 1 ] :

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

där ingen fri variabel ( eng. free v ariable ) ändras ( eng. modifierad ) under påverkan av kommandot . Med den här regeln kan du lägga till godtyckliga predikat om variabler och delar av högen som inte ändras av kommandot . Samtidigt kallade O'Hearn mängden heap som ockuperades av kommandot, termen för engelska. fotavtryck ("avtryck"). Syftet med ramregeln är att utöka argumentet från en mer lokal beskrivning av kommandot till en mer global beskrivning av det omslutande kommandot, kommandot med störst avtryck [1] . $R$ $C$ $C$

Efter att ha fastställt att separationslogiken är ett exempel på logiken för kärveimplikationer, introducerade Yang och Ishtiak den separerande implikationen ( engelsk separating implikation [1] , engelsk trollstav ). Beteckningen säger att om en hög förlängdes med en icke-korsande hög för vilken är sant , då för den resulterande högen kommer det att vara sant [7] . $P-\!\!\!\ast\, Q$ $P$ $F$

Semantiken för logiska bindningar (separerande konjunktion och separerande implikation) innebär en monoid högstruktur [7] .

Parallell Separation Logic (CSL)

Concurrent Separation Logic ( CSL ) är en version av logik som är användbar för verifiering av parallella algoritmer med delat minne. Ursprungligen föreslagen av Peter O'Hearn. Den använder följande regel [16]

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

vilket gör att du kan dra slutsatser i närvaro av oberoende trådar för utförande som kommer åt en separat butik. O'Hearns bevisregler anpassade Tony Hoares tidiga inställning till samtidighet [17] genom att ersätta användningen av räckviddsbegränsningar för att upprätthålla partitionering med resonemang i partitioneringslogik. Förutom att utöka Hoares tillvägagångssätt för heap-pekare, visade O'Hearn att parallell partitioneringslogik dynamiskt kan spåra överföringen av äganderätten till heap-områden mellan processer. Exemplen i hans artikel inkluderar således en pekarpassbuffert och en minneshanterare .

Lokala resonemang kan också förstås i termer av ägaröverlåtelse . Det är lättast att överväga överlåtelse av äganderätt med hjälp av Hoare-monitorreglerna som exempel (du kan se att separationslogiken också är lämplig för distribuerade system). För att komma in i ett kritiskt avsnitt används en separerande konjunktion med , där är resursinvarianten r . När du lämnar det kritiska avsnittet följer den logiska slutsatsen i motsatt riktning [18] : $I_r$ $I_r$

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

I analogi kan vi också betrakta processen att bearbeta ett meddelande som skickas av en annan process med resurser delegerade till denna process, bestämt av fingeravtryck [18] .

En modell för en parallell uppdelningslogik introducerades först av Stephen D. Brookes i en bifogad artikel till O'Hearns papper [19] . Logikens korrekthet ( engelsk soundness ) var ett svårt problem. I synnerhet John Reynolds motexempel visade att en tidigare opublicerad version av logiken misslyckades. Punkten som togs upp av Reynolds exempel beskrivs kortfattat i O'Hearns artikel och mer fullständigt i Brooks's.

O'Hearn och Brooks är medmottagare av Gödelpriset 2016 för uppfinningen av logiken för parallell uppdelning [20] .

Applikationer och implementeringar

Separationens logik har funnit tillämpning i automatiska och interaktiva verifierare av programvara skriven i en imperativ och objektorienterad stil. För detta har lämpliga tillägg till befintliga verifieringsverktyg utvecklats, till exempel, såsom:

Ynot [21] är ett bibliotek för att verifiera imperativa program för Coq .
Predator [22] är en delad logikbaserad programanalysator för att analysera program som innehåller dynamiska listor [23] .

Andra system som använder delad logik: Smallfoot, Space Invader, THOR, SLAyer, HIP, jStar, Xisa, VeriFast, Infer, SeLoger, SLP. Men från och med 2014 finns det inga praktiska teorembevisare som implementerar den fullständiga logiken för partitionering, d.v.s. inklusive en partitioneringsimplikation [7] .

Beroende på typen av användning av systemet kan det delas upp enligt följande [24] :

Användaren skriver manuellt både specifikationen och beviset med hjälp av taktik: interaktiva teoremprover Coq, HOL4, Isabelle/HOL.
Användaren skriver specifikationen och loopinvarianter : oberoende verifieringsverktyg Smallfoot, HIP, Verifast, Jstar.
Användaren skriver bara specifikationen (eller skriver till och med ingenting): formanalysverktyg ( sv . formanalys ) Space Invader, THOR, Xisa, SLAyer.

Anteckningar

↑ 1 2 3 4 5 6 Reynolds, 2002 .
↑ Intuitionistiskt resonemang om delad föränderlig datastruktur. John Reynolds. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in Honor of Sir Tony Hoare
↑ BI som ett påståendespråk för föränderliga datastrukturer. Samin Ishtiaq, Peter O'Hearn. POPL 2001.
↑ Lokala resonemang om program som ändrar datastrukturer. Arkiverad 27 september 2013 på Wayback Machine Peter O'Hearn, John Reynolds, Hongseok Yang . CSL 2001
↑ Några tekniker för att bevisa program som ändrar datastrukturer. RM Burstall. Machine Intelligence 7, 1972.
↑ Logiken av samlade implikationer PW O'Hearn och DJ Pym. Bulletin of Symbolic Logic, 5(2), juni 1999, sid 215-244
↑ 1 2 3 4 Lee, Park, 2014 .
↑ Program och bevis, 2014 .
↑ 12 Reynolds , 2008 .
↑ Parkinson, Bierman, 2005 .
↑ Chris Poskitt Software Verification (hösten 2013) Föreläsning 5: Separation Logic Parts I - II (nedlänk)
↑ 1 2 A Primer on Separation Logic, 2012 .
↑ Tjark Weber (2004). "Mot mekaniserad programverifiering med separationslogik". Computer Science Logic~-- 18:e internationella workshoppen, CSL 2004, 13:e årliga konferensen för EACSL, Karpacz, Polen, september 2004, Proceedings . Föreläsningsanteckningar i datavetenskap. Springer. pp. 250-264. weber04towards . Hämtad 2013-12-06 . |access-date=kräver |url=( hjälp )
↑ Matthew J. Parkinson Lokalt resonemang för Java Arkiverad 23 september 2015 på Wayback Machine , 2005, UCAM-CL-TR-654, ISSN 1476-2986
↑ Föreläsning 24: Pekare och formanalys Arkiverad 29 november 2014 på Wayback Machine , LARA, EPFL
↑ O'Hearn, Peter (2007). "Resurser, samtidighet och lokalt resonemang" (PDF) . Teoretisk datavetenskap . 375 (1-3): 271-307. DOI : 10.1016/j.tcs.2006.12.035 . Arkiverad (PDF) från originalet 2021-03-04 . Hämtad 2021-03-24 . Utfasad parameter används |deadlink=( hjälp )
↑ Hoare, CAR (1972). "Mot en teori om parallell programmering". Operativsystemstekniker. Akademisk press .
↑ 1 2 Étienne Lozes Information as Resource in Separation Logic (otillgänglig länk) , ANR-projekt, utkast
↑ Brookes, Stephen (2007). "En semantik för samtidig separationslogik" (PDF) . Teoretisk datavetenskap . 375 (1-3): 227-270. DOI : 10.1016/j.tcs.2006.12.034 . Arkiverad (PDF) från originalet 2021-05-09 . Hämtad 2021-03-24 . Utfasad parameter används |deadlink=( hjälp )
↑ European Association for Theoretical Computer Science 2016 Gödel-priset Arkiverad 14 juli 2016 på Wayback Machine
↑ Ynot . Hämtad 19 november 2014. Arkiverad från originalet 25 februari 2009. (obestämd)
↑ Rovdjur . Datum för åtkomst: 19 november 2014. Arkiverad från originalet den 25 oktober 2014. (obestämd)
↑ Mutilin V.S., Novikov E.M., Khoroshilov A.V. Översikt över verktyg för statisk verifiering av C-program som tillämpas på drivrutiner för operativsystemet Linux // Proceedings of the Institute for System Programming of the Russian Academy of Sciences. - 2012. - T. 22 , nr 3 . - S. 293-326 .
↑ Cliff Jones (från U. Newcastle), Viktor Vafeiadis (från MPI-SWS) Rely-garanti tänkande & separationslogik Arkiverad 29 november 2014 på Wayback Machine

Litteratur

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 // Verifierad programvara : Teorier, verktyg, experiment : First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zürich, Schweiz, 10-13 oktober 2005, Revised Selected Papers and Discussions / B. Meyer , J. Woodcock - Berlin : Springer Berlin Heidelberg , 2008. - P. 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 (engelska) // POPL '05 : Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programmeing languages Long Beach, CA, USA 12-14 januari 2005 — Nytt York, NY, USA : ACM , 2005. - P. 247-258. - ISBN 978-1-58113-830-6 - doi:10.1145/1040305.1040326
Lee, Wonyeol och Park, Sungwoo. A Proof System for Separation Logic with Magic Wand (engelska) // SIGPLAN Not .. - ACM, 2014. - Vol. 49 , nr. 1 . - S. 477--490 . — ISSN 0362-1340 .
Appel A. , Dockins R. , Hobor A. , Beringer L. , Dodds J. , Blazy S. , Leroy X. Program Logics for Certified Compilers (engelska) - Cambridge University Press , 2014. - 472 sid. — ISBN 978-1-107-04801-0
Ilja Sergey. 8.2 Grunderna i separationslogik // Program och bevis: Mekanisering av matematik med beroende typer . - 2014. - (Föreläsningsanteckningar).
Peter W. O'Hearn. A Primer on Separation Logic (och automatisk programverifiering och analys) // Software Safety and Security; Verktyg för analys och verifiering. - 2012. - Vol. 33. - s. 286-318.

Länkar

Cliff Jones ( Newcastle University ), Viktor Vafeiadis ( MPI-SWS ) Rely-garanti tänkande & separationslogik (eng.) - presentation som väl illustrerar begreppen separationslogik
Matthew Parkinson An Introduction to Separation Logic (engelska) - en presentation där alla de viktigaste aspekterna av separationslogik illustreras: axiom, programexempel med motsvarande diagram, syntax