Erottelulogiikka

Erotuslogiikka , erottelulogiikka ( englanniksi separation logic ) - muodollinen järjestelmä, alirakennelogiikka, jota voidaan soveltaa muuttuvia tietorakenteita ja osoittimia sisältävien ohjelmien varmentamiseen , Hoaren logiikan laajennus . Suunnittelija John Reynolds , Peter O'Hearn , Samin Ishtiaq ja Hongseok Yang [ 1 ] [ 2 ] [ 3] [4] perustuu Rod Burstallin [ 5 ] työhön . Osiointilogiikan väitekieli on nippuimplikaatioiden logiikan erikoistapaus [ 6 ] .

Eräs osiointilogiikan kehitys rinnakkaislaskennassa jaetun muistin kanssa on rinnakkaisosiointilogiikka , jonka ovat kehittäneet O'Hearn ja Stephen D. Brookes .

Erottelulogiikkaan perustuvat tekniikat mahdollistavat suurten ohjelmistoprojektien verifiointijärjestelmien kehittämisen [7] .

Luomisen edellytykset

Hoaren logiikalla on useita rajoituksia, sillä se toimii vain muuttuvilla muuttujilla eikä tue proseduureja tai ensiluokkaista koodia . Suurin rajoitus on kuitenkin osoittimen tuen puute, joka on olennaisin Imperative Program Specification . Osoittimia ja kasaa käytettäessä muuttuvat muuttujat voidaan hylätä antamalla osoittimen arvo paikallisille muuttujille vain kerran [8] .

Vuosina 2000-2002 John Reynolds ja Peter O'Hearn keksivät laajennuksen Hoaren logiikkaan, jakologiikkaan. Alkuperäinen idea oli yksinkertaistaa päättelyä matalan tason pakollisista ohjelmista, joilla on yhteinen muuttuva tietorakenne [9] . Itse termi liittyy tämän logiikan pääajatukseen - tallennustilan ( englanninkielinen tallennus ) jakamisen kuvaus ei-päällekkäisiin komponentteihin. Termiä käytetään sekä predikaattilaskussa , jota jakooperaattori on laajentanut, että Hoaren logiikan laajennuksen tulokseen [1] .

Kuvaus

Erottelulogiikan keskeinen piirre on paikallisen päättelyn (paikallinen päättely) mahdollisuus, joka johtuu lausunnoista spatiaalisten konnektiivien ( eng. spatial connectives ) läsnäolosta kasan osien välillä [10] .

Logiikka antaa sinun työskennellä muodon lauseiden kanssa , jossa: $s,h\models P$

$s$ - muisti (esimerkiksi pinon muodossa [1] ), äärellinen osittainen funktionaalinen kartoitus muuttujista kokonaislukuihin ,
$h$ on kasa, äärellinen osittainen funktionaalinen kuvaus kokonaisluvuista kokonaislukuihin, ja
$P$ - lausunto muistista ja kasosta, eli ohjelman tilasta [12] .

Jotta eri objektien saman osoitteen käyttöä koskevien kieltojen hankalista kuvauksista päästään eroon, on otettu käyttöön uusi looginen operaatio - disjunktiivinen konjunktio , jota merkitään (tai [13] ) ja joka vakuuttaa, että jokainen ehdoista ja täyttyy kasan osa (osoitteellinen varasto ) [9] [14] . Eli totta kasalle , jos tästä kasasta on kaksi osaa ja jolle [15] on totta : $P\ *\ Q$ $P\ \land \!*\ Q$ $P$ $K$ $P\ *\ Q$ $h$ $h_1$ $h_2$

Alueet ja eivät leikkaa; $h_1$ $h_2$
$h$ on ja liitto ; $h_1$ $h_2$
$P$ tosi kaikille osoitteille osoitteesta ; $h_1$
$K$ totta kaikille osoitteille osoitteesta . $h_2$

Yläpuolella ja ymmärretään osittaisina funktioina , jotka antavat arvoja, jotka vastaavat kasan osoitetta. $h_1$ $h_2$

Vahvistaaksesi, että kasa on tyhjä, otetaan käyttöön predikaatti (tässä tapauksessa tietysti ) ja osoitetaan osoitin - . Esimerkiksi seuraavassa, joka on yksi aksioomeista, Hoare -kolmio $emp$ $P\ *\ emp\ \Leftrightarrow \ P$ $e\mapsto x$

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

Edellytyksenä on käyttämätön muistisolu, joka osoitusoperaation seurauksena osoittaa F :een , joka on ilmoitettu jälkiehdossa [12] .

Avain paikalliseen päättelyyn on O'Hearnin [ 1 ] esittämä kehyssääntö :

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

jossa vapaata muuttujaa ( eng. free v ariable ) ei muuteta ( muokattu ) komennon vaikutuksesta . Tämän säännön avulla voit lisätä mielivaltaisia predikaatteja keon muuttujista ja osista, joita komento ei muuta . Samaan aikaan O'Hearn kutsui komennon varaaman kasan määrää termiksi englanti. jalanjälki ("jälki"). Kehyssäännön tarkoitus on laajentaa argumenttia paikallisemmasta komennon kuvauksesta yleisempään kuvaukseen sulkevasta komennosta, komentoon, jolla on suurin jälki [1] . $R$ $C$ $C$

Todettuaan, että erottelulogiikka on esimerkki nivelimplikaatioiden logiikasta, Yang ja Ishtiak esittelivät erottavan implikation ( englanniksi separating impplication [1] , englanniksi magic wand ). Nimitys sanoo, että jos kasaa laajennettiin ei-leikkautuvalla kasalla, jolle on tosi , niin tuloksena olevalle kasalle se on totta [7] . $P-\!\!\!\ast\, Q$ $P$ $K$

Loogisten konnektiivien semantiikka (erotteleva konjunktio ja erottava implikaatio) edellyttää monoidikasarakennetta [ 7] .

Parallel Separation Logic (CSL)

Concurrent Separation Logic ( CSL ) on logiikan versio, jota voidaan soveltaa rinnakkaisten algoritmien varmentamiseen jaetun muistin kanssa. Alunperin ehdotti Peter O'Hearn. Se käyttää seuraavaa sääntöä [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}\))))

jonka avulla voit tehdä johtopäätöksiä itsenäisten suoritussäikeiden läsnä ollessa, jotka käyttävät erillistä kauppaa. O'Hearnin todistesäännöt mukauttivat Tony Hoaren varhaista lähestymistapaa samanaikaisuuteen [17] korvaamalla laajuusrajoitusten käytön osioinnin pakottamiseksi päättelyllä osiointilogiikassa. Sen lisäksi, että O'Hearn laajensi Hoaren lähestymistapaa kasoosoittimiin, se osoitti, että rinnakkaisosiointilogiikka voi dynaamisesti seurata kasa-alueiden omistajuuden siirtoa prosessien välillä. Siten hänen artikkelinsa esimerkkejä ovat osoittimen välityspuskuri ja muistinhallinta .

Paikallinen päättely voidaan ymmärtää myös omistusoikeuden siirtymisenä . Omistuksen siirtoa on helpoin harkita esimerkkinä Hoaren monitorointisäännöillä (näet, että erottelulogiikka sopii myös hajautetuille järjestelmille). Kriittisen osan syöttämiseksi käytetään erotuskonjunktiota , jossa on resurssin invariantti r . Kriittisestä osiosta poistuttaessa seuraa looginen johtopäätös päinvastaiseen suuntaan [18] : $I_r$ $I_r$

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

Analogisesti voimme myös tarkastella prosessia, jossa prosessi käsittelee toisen prosessin lähettämää viestiä prosessille delegoiduilla resursseilla, jotka määritetään sormenjälkien avulla [18] .

Stephen D. Brookes esitteli ensimmäisen kerran mallin rinnakkaisosiointilogiikasta O'Hearnin artikkelin mukana [ 19] . Logiikan oikeellisuus ( englanniksi soundness ) oli vaikea ongelma. Erityisesti John Reynoldsin vastaesimerkki osoitti logiikan aikaisemman, julkaisemattoman version epäonnistumisen. Reynoldsin esimerkin esille tuoma seikka on kuvattu lyhyesti O'Hearnin artikkelissa ja täydellisemmin Brooksin artikkelissa.

O'Hearn ja Brooks ovat saaneet vuoden 2016 Gödel-palkinnon rinnakkaisosioinnin logiikan keksimisestä [20] .

Sovellukset ja toteutukset

Erottamisen logiikka on löytänyt sovelluksen automaattisissa ja interaktiivisissa todentajissa, jotka on kirjoitettu imperatiiviseen ja olio- tyyliin. Tätä varten kehitettiin sopivia lisäyksiä olemassa oleviin varmennustyökaluihin, kuten esimerkiksi:

Ynot [21] on kirjasto Coqin pakollisten ohjelmien tarkistamiseen .
Predator [22] on jaettuun logiikkaan perustuva ohjelma-analysaattori dynaamisia listoja sisältävien ohjelmien analysointiin [23] .

Muut jaettua logiikkaa käyttävät järjestelmät: Smallfoot, Space Invader, THOR, SLAyer, HIP, jStar, Xisa, VeriFast, Infer, SeLoger, SLP. Vuodesta 2014 lähtien ei kuitenkaan ole olemassa käytännön lauseiden todistajia, jotka toteuttaisivat osioinnin täyden logiikan, eli sisältäen osiointiimplikaatiota [7] .

Järjestelmän käytön luonteen mukaan se voidaan jakaa seuraavasti [24] :

Käyttäjä kirjoittaa manuaalisesti sekä spesifikaation että todisteen taktiikalla: interaktiiviset lauseen todistajat Coq, HOL4, Isabelle/HOL.
Käyttäjä kirjoittaa spesifikaatiot ja silmukkainvariantit : riippumattomat tarkistustyökalut Smallfoot, HIP, Verifast, Jstar.
Käyttäjä kirjoittaa vain määrittelyn (tai ei edes kirjoita mitään): muotoanalyysityökalut ( eng . shape analysis ) Space Invader, THOR, Xisa, SLAyer.

Muistiinpanot

↑ 1 2 3 4 5 6 Reynolds, 2002 .
↑ Intuitionistinen päättely jaetusta muuttuvasta tietorakenteesta. John Reynolds. Millennial Perspectives in Computer Science, Proceeding of 1999 Oxford-Microsoft Symposium Sir Tony Hoaren kunniaksi
↑ BI muuttuvien tietorakenteiden vahvistuskielenä. Samin Ishtiaq, Peter O'Hearn. POPL 2001.
↑ Paikalliset perustelut ohjelmista, jotka muuttavat tietorakenteita. Arkistoitu 27. syyskuuta 2013 Wayback Machinessa Peter O'Hearn, John Reynolds, Hongseok Yang . CSL 2001
↑ Joitakin tekniikoita tietorakenteita muuttavien ohjelmien todistamiseen. RM Burstall. Machine Intelligence 7, 1972.
↑ The Logic of Bunched Impplications PW O'Hearn ja DJ Pym. Bulletin of Symbolic Logic, 5(2), kesäkuu 1999, s. 215-244
↑ 1 2 3 4 Lee, Park, 2014 .
↑ Ohjelmat ja todisteet, 2014 .
↑ 12 Reynolds , 2008 .
↑ Parkinson, Bierman, 2005 .
↑ Chris Poskitt Software Verification (Syksy 2013) Luento 5: Erotuslogiikan osat I - II (downlink)
↑ 1 2 A Primer on Separation Logic, 2012 .
↑ Tjark Weber (2004). "Kohti koneistettua ohjelman vahvistusta erottelulogiikalla". Computer Science Logic~-- 18th International Workshop, CSL 2004, 13th Annual Conference of EACSL, Karpacz, Puola, syyskuu 2004, Proceedings . Tietojenkäsittelytieteen luentomuistiinpanot. Springer. s. 250-264. weber04 kohti . Haettu 2013-12-06 . |access-date=vaatii |url=( apua )
↑ Matthew J. Parkinson Paikalliset perustelut Javalle Arkistoitu 23. syyskuuta 2015 Wayback Machinessa , 2005, UCAM-CL-TR-654, ISSN 1476-2986
↑ Luento 24: Osoitin- ja muotoanalyysi Arkistoitu 29. marraskuuta 2014 Wayback Machinessa , LARA, EPFL
↑ O'Hearn, Peter (2007). "Resurssit, samanaikaisuus ja paikallinen päättely" (PDF) . Teoreettinen tietojenkäsittelytiede . 375 (1-3): 271-307. DOI : 10.1016/j.tcs.2006.12.035 . Arkistoitu (PDF) alkuperäisestä 2021-03-04 . Haettu 24.03.2021 . Käytöstä poistettu parametri |deadlink=( ohje )
↑ Hoare, CAR (1972). "Kohti rinnakkaisohjelmoinnin teoriaa". Käyttöjärjestelmän tekniikat. Akateeminen Lehdistö .
↑ 1 2 Étienne menettää tiedon erottelulogiikan resurssina (linkki ei saatavilla) , ANR-projekti, luonnos
↑ Brookes, Stephen (2007). "Semantics for Concurrent Separation Logic" (PDF) . Teoreettinen tietojenkäsittelytiede . 375 (1-3): 227-270. DOI : 10.1016/j.tcs.2006.12.034 . Arkistoitu (PDF) alkuperäisestä 2021-05-09 . Haettu 24.03.2021 . Käytöstä poistettu parametri |deadlink=( ohje )
↑ European Association for Theoretical Computer Science 2016 Gödel-palkinto arkistoitu 14. heinäkuuta 2016 Wayback Machinessa
↑ Ei . Haettu 19. marraskuuta 2014. Arkistoitu alkuperäisestä 25. helmikuuta 2009. (määrätön)
↑ Petoeläimet . Käyttöpäivä: 19. marraskuuta 2014. Arkistoitu alkuperäisestä 25. lokakuuta 2014. (määrätön)
↑ Mutilin V.S., Novikov E.M., Khoroshilov A.V. Yleiskatsaus työkaluista C-ohjelmien staattiseen varmentamiseen Linux-käyttöjärjestelmän laiteajureihin sovellettuina // Proceedings of Institute for System Programming of the Russian Sciences Academy. - 2012. - T. 22 , nro 3 . - S. 293-326 .
↑ Cliff Jones (U. Newcastlesta), Viktor Vafeiadis (MPI-SWS:stä) Luota ajatteluun ja erottelulogiikkaan . Arkistoitu 29. marraskuuta 2014 Wayback Machinessa

Kirjallisuus

Reynolds J. C. Separation Logic: Logic for Shared Mutable Data Structures // LICS '02 :of 17th Annual 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. Katsaus erottelulogiikkaan // Varmennettu ohjelmisto : teoriat, työkalut, kokeet : ensimmäinen IFIP TC 2/WG 2.3 -konferenssi, VSTTE 2005, Zürich, Sveitsi, 10.–13. lokakuuta 2005, tarkistetut valitut paperit / B. -keskustelut , J. Woodcock - Berlin : Springer Berlin Heidelberg , 2008. - P. 460-469. - ( Lecture Notes in Computer Science ; Voi. 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. Erotuslogiikka ja abstraktio (englanniksi) // POPL '05 : Proceedings of the 32nd ACM SIGPLAN-SIGACT -symposium on Principles of Programming Languages (Long Beach, CA, USA 12.-14.1.2005 – Uusi ) York, NY, USA : ACM , 2005. - s. 247-258. - ISBN 978-1-58113-830-6 - doi:10.1145/1040305.1040326
Lee, Wonyeol ja Park, Sungwoo. A Proof System for Separation Logic with Magic Wand (englanniksi) // SIGPLAN Not .. - ACM, 2014. - Vol. 49 , ei. 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 (englanniksi) - Cambridge University Press , 2014. - 472 s. — ISBN 978-1-107-04801-0
Ilja Sergei. 8.2 Erotuslogiikan perusteet // Ohjelmat ja todistukset: Matematiikan mekanisointi riippuvilla tyypeillä . - 2014. - (Luentomuistiinpanot).
Peter W. O'Hearn. A Primer on Separation Logic (ja automaattinen ohjelman tarkistus ja analyysi) // Ohjelmiston turvallisuus; Analyysi- ja todentamistyökalut. - 2012. - Vol. 33. - s. 286-318.

Linkit

Cliff Jones ( Newcastlen yliopisto ), Viktor Vafeiadis ( MPI-SWS ) Luota ajatteluun ja erottelulogiikkaan (eng.) - esitys havainnollistaa hyvin erottelulogiikan käsitteitä
Matthew Parkinson An Introduction to Separation Logic (englanniksi) - esitys, jossa havainnollistetaan kaikki erottelulogiikan pääkohdat: aksioomit, ohjelmaesimerkit vastaavilla kaavioilla, syntaksi