Elválasztási logika

Elválasztási logika , elválasztási logika ( angol szeparációs logika ) - formális rendszer, szubstrukturális logika, amely módosítható adatstruktúrákat és mutatókat tartalmazó programok ellenőrzésére alkalmazható, a Hoare-féle logika kiterjesztése . Tervezte : John Reynolds , Peter O'Hearn , Samin Ishtiaq és Hongseok Yang [ 1 ] [ 2 ] [ 3] [4] Rod Burstall munkái alapján [ 5 ] . A particionálási logika állítási nyelve a kötegelt implikációk logikájának egy speciális esete [ 6 ] .

A megosztott memóriával történő párhuzamos számítástechnika particionálási logikájának egy evolúciója a párhuzamos particionálási logika , amelyet O'Hearn és Stephen D. Brookes fejlesztett ki .

Az elválasztás logikáján alapuló technológiák lehetővé teszik nagy szoftverprojektek verifikálására szolgáló rendszerek kifejlesztését [7] .

A létrehozás előfeltételei

A Hoare logikájának számos korlátozása van, csak változó változókon működik, és nem támogatja az eljárásokat vagy az első osztályú kódot . A legnagyobb korlátozás azonban a mutató támogatásának hiánya, ami leginkább az Imperative Program Specifikáció szempontjából releváns . A mutatók és a kupac használata esetén a változó változók elhagyhatók, ha a lokális változókhoz csak egyszer adunk mutatóértéket [8] .

2000-2002-ben John Reynolds és Peter O'Hearn Hoare logikájának kiterjesztésével, a felosztási logikával állt elő. Az eredeti ötlet az volt, hogy leegyszerűsítsék az alacsony szintű kötelező programokkal kapcsolatos érvelést egy közös, változtatható adatstruktúrával [9] . Maga a kifejezés ennek a logikának a fő gondolatához kapcsolódik - a tárolás ( angol tárolás ) nem átfedő komponensekre való felosztásának leírásához. A kifejezést mind az osztásoperátor által kibővített predikátumszámításra , mind a Hoare-féle logika kiterjesztésének eredményére [1] használják .

Leírás

Az elválasztás logikájának kulcsfontosságú jellemzője a lokális érvelés (lokális érvelés) lehetősége a halom részei közötti térbeli konnektívumok ( eng. spatial connectives ) kijelentéseiben [10] .

A logika lehetővé teszi, hogy olyan utasításokkal dolgozzon , ahol: $s,h\models P$

$s$ - memória (például verem [1] formájában ), véges parciális funkcionális leképezés változókból egész számokra ,
$h$ egy kupac, véges parciális funkcionális leképezés egész számokról egész számokra, és
$P$ - állítás a memóriáról és a kupacról, vagyis a program állapotáról [12] .

Az azonos címek különböző objektumok általi használatára vonatkozó tilalmak nehézkes leírásainak leküzdésére egy új logikai műveletet vezettünk be - egy diszjunkt kötőszót , amelyet (vagy [13] ) jelöl, és azt állítja, hogy a és minden feltétel teljesül. a kupac része (címzett tároló ) [9] [14] . Vagyis igaz egy kupacra , ha ennek a kupacnak két része van, és amelyre a [15] igaz : $P\ *\ Q$ $P\ \land \!*\ Q$ $P$ $K$ $P\ *\ Q$ $h$ $h_1$ $h_2$

A régiók és nem metszik egymást; $h_1$ $h_2$
$h$ az és uniója ; $h_1$ $h_2$
$P$ igaz minden címre innen ; $h_1$
$K$ igaz az összes címre . $h_2$

A fenti és részfüggvények alatt értendők, amelyek a kupacban lévő címnek megfelelő értékeket adnak. $h_1$ $h_2$

Annak állítása érdekében, hogy a kupac üres, egy predikátumot vezetünk be (ebben az esetben nyilvánvalóan ), és egy mutatót jelölünk ki - . Például a következőkben, amely az egyik axióma, a Hoare-hármas $emp$ $P\ *\ emp\ \Leftrightarrow \ P$ $e\mapsto x$

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

előfeltétele a nem használt memóriacella, amely a hozzárendelési művelet eredményeként F -re mutat, amit a [12] utófeltételben közölünk .

A helyi érvelés kulcsa az O'Hearn által bevezetett keretszabály [ 1 ] :

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

amelyben egyetlen szabad változó ( angol . free v ariable ) sem módosul ( módosul ) a parancs hatására . Ezzel a szabálysal tetszőleges predikátumokat adhat hozzá azokhoz a változókhoz és a kupac részeihez, amelyeket a parancs nem módosít . Ugyanakkor O'Hearn a parancs által elfoglalt kupac mennyiségét angol kifejezésnek nevezte. lábnyom ("lenyomat"). A keretszabály célja az argumentum kiterjesztése a parancs lokálisabb leírásától a befoglaló parancs globálisabb leírására, a legnagyobb impresszumú parancsra [1] . $R$ $C$ $C$

Miután megállapították, hogy az elválasztás logikája a köteg-implikációk logikájának egyik példája, Yang és Ishtiak bevezette az elválasztó implikációt ( angolul separating impplication [1] , angol varázspálca ). A megnevezés azt mondja, hogy ha egy kupacot kiterjesztettek egy nem metsző kupacra, amelyre igaz , akkor a kapott kupacra igaz lesz [7] . $P-\!\!\!\ast\, Q$ $P$ $K$

A logikai konnektívumok szemantikája (elválasztó kötőszó és elválasztó implikáció) monoid halomszerkezetet foglal magában [7] .

Parallel Separation Logic (CSL)

A Concurrent Separation Logic ( CSL ) a logika egy olyan változata, amely a megosztott memóriával rendelkező párhuzamos algoritmusok ellenőrzésére használható. Eredetileg Peter O'Hearn javasolta. A következő szabályt használja [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}\))))

amely lehetővé teszi következtetések levonását egy külön tárolóhoz hozzáférő független végrehajtási szálak jelenlétében. Az O'Hearn-féle bizonyítási szabályok adaptálták Tony Hoare korai párhuzamossági megközelítését [17] azáltal, hogy a particionálás kikényszerítésére szolgáló hatókör-megszorításokat a particionálási logikában való érveléssel helyettesítették. Amellett, hogy Hoare megközelítését kiterjesztette a halommutatókra, O'Hearn megmutatta, hogy a párhuzamos particionálási logika képes dinamikusan nyomon követni a kupacterületek tulajdonjogának átruházását a folyamatok között. Így a cikkében szereplő példák között szerepel egy pointer pass puffer és egy memóriakezelő .

A helyi érvelés a tulajdonjog átruházásával is értelmezhető . A tulajdonjog átruházását a legegyszerűbben a Hoare monitorszabályok példájának segítségével lehet megfontolni (látható, hogy a szétválasztási logika alkalmas elosztott rendszerekre is). A kritikus szakaszba való belépéshez elválasztó kötőszót használunk a -val , ahol az r erőforrás-invariáns . A kritikus szakaszból kilépve a logikai következtetés az ellenkező irányban következik [18] : $I_r$ $I_r$

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

Analógia alapján tekinthetjük egy másik folyamat által küldött üzenetnek egy folyamat általi feldolgozását is, ehhez a folyamathoz delegált, ujjlenyomatokkal meghatározott erőforrásokkal [18] .

A párhuzamos particionálási logika modelljét először Stephen D. Brookes mutatta be O'Hearn tanulmányához [ 19] . A logika helyessége ( angolul megalapozottsága ) nehéz probléma volt. Különösen John Reynolds ellenpéldája mutatta be a logika egy korábbi, kiadatlan változatának kudarcát. A Reynolds példája által felvetett kérdést O'Hearn cikkében, részletesebben Brooks cikkében ismerteti.

O'Hearn és Brooks a 2016 -os Gödel-díj társdíjasai a párhuzamos particionálás logikájának feltalálásáért [20] .

Alkalmazások és megvalósítások

Az elválasztás logikája alkalmazásra talált a kötelező és objektum-orientált stílusban írt szoftverek automatikus és interaktív hitelesítőiben. Ehhez megfelelő kiegészítéseket fejlesztettek ki a meglévő ellenőrző eszközökhöz, például:

Az Ynot [21] egy könyvtár a Coq kötelező programjainak ellenőrzésére .
A Predator [22] egy osztott logikán alapuló programelemző dinamikus listákat tartalmazó programok elemzésére [23] .

Egyéb osztott logikát használó rendszerek: Smallfoot, Space Invader, THOR, SLAyer, HIP, jStar, Xisa, VeriFast, Infer, SeLoger, SLP. 2014-től azonban nem léteznek olyan gyakorlati tételbizonyítók, amelyek a particionálás teljes logikáját megvalósítanák, azaz tartalmaznának particionálási implikációt [7] .

A rendszer használatának jellege szerint a következőképpen osztható fel [24] :

A felhasználó manuálisan írja meg a specifikációt és a bizonyítást is taktikával: interaktív tételbizonyítók Coq, HOL4, Isabelle/HOL.
A felhasználó írja a specifikációt és a ciklusinvariánsokat : független ellenőrző eszközök Smallfoot, HIP, Verifast, Jstar.
A felhasználó csak a specifikációt írja (vagy nem is ír semmit): alakelemző eszközök ( eng . shape analysis ) Space Invader, THOR, Xisa, SLAyer.

Jegyzetek

↑ 1 2 3 4 5 6 Reynolds, 2002 .
↑ Intuicionista érvelés a megosztott változó adatszerkezetről. John Reynolds. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium of Honor of Sir Tony Hoare
↑ A BI mint állítási nyelv a változó adatstruktúrákhoz. Samin Ishtiaq, Peter O'Hearn. POPL 2001.
↑ Helyi érvelés az adatstruktúrákat megváltoztató programokról. Archivált : 2013. szeptember 27. a Wayback Machine -nél Peter O'Hearn, John Reynolds, Hongseok Yang . CSL 2001
↑ Néhány technika az adatstruktúrákat megváltoztató programok bizonyítására. RM Burstall. Machine Intelligence 7, 1972.
↑ The Logic of Bunched Impplications PW O'Hearn és DJ Pym. Bulletin of Symbolic Logic, 5(2), 1999. június, 215-244.
↑ 1 2 3 4 Lee, Park, 2014 .
↑ Programok és bizonyítványok, 2014 .
↑ 12 Reynolds , 2008 .
↑ Parkinson, Bierman, 2005 .
↑ Chris Poskitt szoftverellenőrzés (2013. ősz) 5. előadás: Elválasztási logika I-II. rész (lefelé irányuló kapcsolat)
↑ 1 2 A Primer on Separation Logic, 2012 .
↑ Tjark Weber (2004). „A gépesített programellenőrzés elválasztási logikával felé”. Computer Science Logic~-- 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 2004, Proceedings . Előadásjegyzetek számítástechnikából. Springer. pp. 250-264. weber04 felé . Letöltve: 2013-12-06 . |access-date=|url=( segítségre van szüksége )
↑ Matthew J. Parkinson A Java helyi érvelése Archiválva : 2015. szeptember 23., a Wayback Machine , 2005, UCAM-CL-TR-654, ISSN 1476-2986
↑ 24. előadás: Mutató- és alakelemzés Archiválva : 2014. november 29., the Wayback Machine , LARA, EPFL
↑ O'Hearn, Peter (2007). „Források, párhuzamosság és helyi érvelés” (PDF) . Elméleti számítástechnika . 375 (1-3): 271-307. DOI : 10.1016/j.tcs.2006.12.035 . Archivált (PDF) az eredetiből ekkor: 2021-03-04 . Letöltve: 2021-03-24 . Elavult használt paraméter |deadlink=( súgó )
↑ Hoare, CAR (1972). „A párhuzamos programozás elmélete felé”. Operációs rendszer technikák. Akadémiai Kiadó .
↑ 1 2 Étienne elveszíti az információt, mint erőforrást az elválasztási logikában ( nem elérhető hivatkozás)
↑ Brookes, Stephen (2007). „A szemantika egyidejű elválasztási logikához” (PDF) . Elméleti számítástechnika . 375 (1-3): 227-270. DOI : 10.1016/j.tcs.2006.12.034 . Archivált (PDF) az eredetiből ekkor: 2021-05-09 . Letöltve: 2021-03-24 . Elavult használt paraméter |deadlink=( súgó )
↑ European Association for Theoretical Computer Science 2016 Gödel-díj archiválva 2016. július 14-én a Wayback Machine -nél
↑ Ynot . Letöltve: 2014. november 19. Az eredetiből archiválva : 2009. február 25.. (határozatlan)
↑ Ragadozók . Hozzáférés időpontja: 2014. november 19. Az eredetiből archiválva : 2014. október 25. (határozatlan)
↑ Mutilin V.S., Novikov E.M., Khoroshilov A.V. A C-programok statikus ellenőrzésére szolgáló eszközök áttekintése a Linux operációs rendszer eszközillesztőire vonatkozóan // Az Orosz Tudományos Akadémia Rendszerprogramozási Intézetének közleménye. - 2012. - T. 22 , 3. sz . - S. 293-326 .
↑ Cliff Jones (az U. Newcastle-től), Viktor Vafeiadis (az MPI-SWS-től) Rely-garantálja a gondolkodást és az elválasztási logikát Archiválva : 2014. november 29. a Wayback Machine -nél

Irodalom

Reynolds J. C. Separation Logic: A Logic for Shared Mutable Data Structures // LICS '02 :of the 17th Annual Annual IEEE Symposium on Logic in Computer Science - Washington, DC, USA : IEEE Computer Society , 2002. - P. 55-74. - ISBN 978-0-7695-1483-3 - doi:10.1109/LICS.2002.1029817
Reynolds J. C. A szétválasztási logika áttekintése // Ellenőrzött szoftver : elméletek, eszközök, kísérletek : első IFIP TC 2 / WG 2.3 konferencia, VSTTE 2005, Zürich, Svájc, 2005. október 10-13., Válogatott dokumentumok és viták felülvizsgált , J. Woodcock - Berlin : Springer Berlin Heidelberg , 2008. - P. 460-469. - ( Számítástechnikai előadások jegyzetei ; 4171. kötet) - ISBN 978-3-540-69147-1 - ISSN 0302-9743 ; 1611-3349 - doi:10.1007/978-3-540-69149-5_49
Parkinson M. , Bierman G. Elválasztási logika és absztrakció (angol) // POPL '05 : Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach, CA, USA, 2005. január 12-14.) – Új York, NY, USA : ACM , 2005. - P. 247-258. - ISBN 978-1-58113-830-6 - doi:10.1145/1040305.1040326
Lee, Wonyeol és Park, Sungwoo. A Proof System for Separation Logic with Magic Wand (angol) // SIGPLAN Not .. - ACM, 2014. - Vol. 49 , sz. 1 . - P. 477--490 . — ISSN 0362-1340 .
Appel A. , Dockins R. , Hobor A. , Beringer L. , Dodds J. , Blazy S. , Leroy X. Program Logics for Certified Compilers (angol) - Cambridge University Press , 2014. - 472 p. — ISBN 978-1-107-04801-0
Ilja Szergej. 8.2 Az elválasztási logika alapjai // Programok és bizonyítások: A matematika gépesítése függő típusokkal . - 2014. - (Előadási jegyzetek).
Peter W. O'Hearn. A Primer on Separation Logic (és az automatikus programellenőrzés és -elemzés) // Szoftverbiztonság; Eszközök az elemzéshez és ellenőrzéshez. - 2012. - Kt. 33. - P. 286-318.

Linkek

Cliff Jones ( Newcastle University ), Viktor Vafeiadis ( MPI-SWS ) Rely-guarantee thinking & szeparációs logika (eng.) - előadás jól szemlélteti az elválasztási logika fogalmait
Matthew Parkinson Introduction to Separation Logic (angol) - egy előadás, amelyben az elválasztási logika minden fő aspektusát szemléltetjük: axiómák, programpéldák megfelelő diagramokkal, szintaxis