Logica de separare

Logica de separare , logica de separare (logica de separare în engleză ) - sistem formal, logică substructurală, aplicabil la verificarea programelor care conțin structuri de date mutabile și pointeri , o extensie a logicii lui Hoare . Proiectat de John Reynolds , Peter O'Hearn , Samin Ishtiaq și Hongseok Yang [ 1 ] [ 2 ] [ 3 ] [4] bazat pe munca lui Rod Burstall [ 5 ] . Limbajul de aserție al logicii partiționării este un caz special al logicii implicațiilor grupate [ 6 ] .

O evoluție a logicii de partiționare pentru calculul paralel cu memorie partajată este logica de partiționare paralelă , dezvoltată de O'Hearn și Stephen D. Brookes .

Tehnologiile bazate pe logica separării fac posibilă dezvoltarea sistemelor de verificare a proiectelor software mari [7] .

Condiții preliminare pentru creare

Logica lui Hoare are o serie de limitări, care operează numai pe variabile mutabile și nu acceptă proceduri sau cod de primă clasă . Cu toate acestea, cea mai mare limitare este lipsa suportului pentru pointer , care este cea mai relevantă pentru specificația imperativă a programului . În cazul utilizării pointerilor și a heap -ului , variabilele mutabile pot fi abandonate prin atribuirea unei valori de pointer variabilelor locale o singură dată [8] .

În 2000-2002, John Reynolds și Peter O'Hearn au venit cu o extensie a logicii lui Hoare, logica diviziunii. Ideea inițială a fost de a simplifica raționamentul despre programele imperative de nivel scăzut cu o structură comună de date mutabilă [9] . Termenul în sine este asociat cu ideea principală a acestei logici - descrierea divizării stocării ( stocare în limba engleză ) în componente care nu se suprapun. Termenul este folosit atât în raport cu calculul predicat , extins prin operatorul de împărțire , cât și cu rezultatul unei extensii a logicii lui Hoare [1] .

Descriere

O trăsătură cheie a logicii separării este posibilitatea raționamentului local (raționamentul local) datorită prezenței în enunțuri a conectivelor spațiale ( eng. conective spațiale ) între părți ale grămezii [10] .

Logica vă permite să lucrați cu instrucțiuni de forma , unde: $s,h\modele P$

$s$ - memorie (de exemplu, sub forma unei stive [1] ), o mapare funcțională parțială finită de la variabile la numere întregi ,
$h$ este un heap, o mapare funcțională parțială finită de la numere întregi la numere întregi și
$P$ - o afirmație despre memorie și heap, adică despre starea programului [12] .

Pentru a depăși descrierile greoaie ale interdicțiilor de utilizare a aceleiași adrese de către diferite obiecte, a fost introdusă o nouă operație logică - o conjuncție disjunctă , notată cu (sau [13] ) și care afirmă că fiecare dintre condițiile și sunt îndeplinite în ea parte din heap (stocare adresată) [9] [14] . Adică, adevărat pentru o grămadă dacă există două părți ale acestui morman și pentru care [15] este adevărat : $P\ *\ Q$ $P\ \land \!*\ Q$ $P$ $Q$ $P\ *\ Q$ $h$ $h_1$ $h_2$

Regiunile și nu se intersectează; $h_1$ $h_2$
$h$ este uniunea dintre și ; $h_1$ $h_2$
$P$ adevărat pentru toate adresele de la ; $h_1$
$Q$ adevărat pentru toate adresele de la . $h_2$

Mai sus și sunt înțelese ca funcții parțiale care dau valori corespunzătoare unei adrese din heap. $h_1$ $h_2$

Pentru a afirma că heap-ul este gol, se introduce un predicat (în acest caz, evident, ), și pentru a desemna un pointer - . De exemplu, în cele ce urmează, care este una dintre axiome, triplul Hoare $emp$ $P\ *\emp\\Leftrightarrow \P$ $e\mapsto x$

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

condiția preliminară este celula de memorie neutilizată, care, ca urmare a operației de atribuire, indică către F , care este menționat în postcondiția [12] .

Cheia raționamentului local este regula cadru introdusă de O'Hearn [ 1 ] :

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

în care nicio variabilă liberă ( ing . variabilă liberă ) nu este modificată ( ing. modificată ) sub influenţa comenzii . Folosind această regulă, puteți adăuga predicate arbitrare despre variabilele și părțile heap-ului care nu sunt modificate de comanda . În același timp, O'Hearn a numit cantitatea de grămadă ocupată de comandă termenul englez. amprentă („amprentă”). Scopul regulii cadru este acela de a extinde argumentul de la o descriere mai locală a comenzii la o descriere mai globală a comenzii incluse, comanda cu cea mai mare amprentă [1] . $R$ $C$ $C$

După ce s-a stabilit că logica separării este un exemplu al logicii implicațiilor snopului, Yang și Ishtiak au introdus implicația de separare ( în engleză separare implicație [1] , engleză magic wand ). Denumirea spune că dacă o grămadă a fost extinsă printr-o grămadă neintersectată pentru care este adevărată , atunci pentru grămada rezultată va fi adevărată [7] . $P-\!\!\!\ast\, Q$ $P$ $Q$

Semantica conjunctivelor logice (conjuncție de separare și implicație de separare) implică o structură heap monoid [7] .

Logica de separare paralelă (CSL)

Logica de separare simultană ( CSL ) este o versiune a logicii aplicabile pentru verificarea algoritmilor paraleli cu memorie partajată. Propus inițial de Peter O'Hearn. Utilizează următoarea regulă [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}\))))

care vă permite să trageți concluzii în prezența unor fire independente de execuție accesând un depozit separat. Regulile de demonstrare ale lui O'Hearn au adaptat abordarea timpurie a concurenței a lui Tony Hoare [17] prin înlocuirea utilizării constrângerilor de domeniu pentru a impune partiționarea cu raționament în logica partiționării. Pe lângă extinderea abordării lui Hoare cu privire la pointerii heap, O'Hearn a arătat că logica de partiționare paralelă poate urmări în mod dinamic transferul de proprietate asupra zonelor heap între procese. Astfel, exemplele din articolul său includ un buffer de trecere a indicatorului și un manager de memorie .

Raționamentul local poate fi înțeles și în termeni de transfer al proprietății . Cel mai ușor este să luați în considerare transferul de proprietate folosind regulile monitorului Hoare ca exemplu (puteți vedea că logica de separare este potrivită și pentru sistemele distribuite ). Pentru a intra într-o secțiune critică , se folosește o conjuncție de separare cu , unde este invariantul de resursă r . La ieșirea din secțiunea critică, concluzia logică urmează în sens invers [18] : $I_r$ $I_r$

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

Prin analogie, putem considera și procesul de procesare de către un proces un mesaj transmis de un alt proces cu resurse delegate acestui proces, determinate de amprente [18] .

Un model pentru o logică de partiționare paralelă a fost introdus pentru prima dată de Stephen D. Brookes într- o lucrare care însoțește lucrarea lui O'Hearn [19] . Corectitudinea logicii a fost o problemă dificilă. În special, contraexemplul lui John Reynolds a arătat eșecul unei versiuni anterioare, nepublicate, a logicii. Punctul ridicat de exemplul lui Reynolds este descris pe scurt în articolul lui O'Hearn și mai pe deplin în cel al lui Brooks.

O'Hearn și Brooks sunt co-beneficiari ai Premiului Gödel 2016 pentru inventarea logicii partiționării paralele [20] .

Aplicații și implementări

Logica separării și-a găsit aplicație în verificatoarele automate și interactive ale software-ului scris într-un stil imperativ și orientat pe obiecte . Pentru aceasta, au fost dezvoltate completări adecvate la instrumentele de verificare existente, de exemplu, cum ar fi:

Ynot [21] este o bibliotecă pentru verificarea programelor imperative pentru Coq .
Predator [22] este un analizor de programe bazat pe logica divizată pentru analiza programelor care conțin liste dinamice [23] .

Alte sisteme care folosesc logica split: Smallfoot, Space Invader, THOR, SLAyer, HIP, jStar, Xisa, VeriFast, Infer, SeLoger, SLP. Cu toate acestea, din 2014, nu există dovezitori de teoreme practice care să implementeze logica completă a partiționării, adică să includă o implicație de partiționare [7] .

În funcție de natura utilizării sistemului, acesta poate fi împărțit după cum urmează [24] :

Utilizatorul scrie manual atât specificația, cât și demonstrația folosind tactici: demonstratori interactiv de teoreme Coq, HOL4, Isabelle/HOL.
Utilizatorul scrie specificațiile și invarianții buclei : instrumente independente de verificare Smallfoot, HIP, Verifast, Jstar.
Utilizatorul scrie doar specificația (sau chiar nu scrie nimic): instrumente de analiză a formei ( ing . shape analysis ) Space Invader, THOR, Xisa, SLAyer.

Note

↑ 1 2 3 4 5 6 Reynolds, 2002 .
↑ Raționament intuitiv despre structura de date mutabilă partajată. John Reynolds. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in onoarea lui Sir Tony Hoare
↑ BI ca limbaj de afirmare pentru structurile de date mutabile. Samin Ishtiaq, Peter O'Hearn. POPL 2001.
↑ Raționamentul local despre programele care modifică structurile de date. Arhivat pe 27 septembrie 2013 la Wayback Machine Peter O'Hearn, John Reynolds, Hongseok Yang . CSL 2001
↑ Câteva tehnici de demonstrare a programelor care modifică structurile de date. RM Burstall. Machine Intelligence 7, 1972.
↑ Logic of Bunched Implications PW O'Hearn și DJ Pym. Buletinul de logică simbolică, 5(2), iunie 1999, pp215-244
↑ 1 2 3 4 Lee, Park, 2014 .
↑ Programs and Proofs, 2014 .
↑ 12 Reynolds , 2008 .
↑ Parkinson, Bierman, 2005 .
↑ Chris Poskitt Software Verification (toamna 2013) Curs 5: Separation Logic Parts I - II (downlink)
↑ 1 2 A Primer on Separation Logic, 2012 .
↑ Tjark Weber (2004). „Spre verificarea mecanizată a programelor cu logică de separare”. Computer Science Logic~-- 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Polonia, September 2004, Proceedings . Note de curs în informatică. Springer. pp. 250-264. weber04spre . Accesat 2013-12-06 . |access-date=necesită |url=( ajutor )
^ Matthew J. Parkinson Local reasoning for Java Arhivat 23 septembrie 2015 la Wayback Machine , 2005, UCAM-CL-TR-654, ISSN 1476-2986
↑ Curs 24: Pointer and shape analysis Arhivat 29 noiembrie 2014 la Wayback Machine , LARA, EPFL
↑ O'Hearn, Peter (2007). „Resurse, concurență și raționament local” (PDF) . Informatica teoretica . 375 (1-3): 271-307. DOI : 10.1016/j.tcs.2006.12.035 . Arhivat (PDF) din original pe 2021-03-04 . Preluat 2021-03-24 . Parametrul depreciat folosit |deadlink=( ajutor )
↑ Hoare, CAR (1972). „Către o teorie a programării paralele”. Tehnici ale sistemului de operare. Presa Academică .
↑ 1 2 Étienne Lozes Information as Resource in Separation Logic (link indisponibil) , proiect ANR, schiță
↑ Brookes, Stephen (2007). „O semantică pentru logica separării concurente” (PDF) . Informatica teoretica . 375 (1-3): 227-270. DOI : 10.1016/j.tcs.2006.12.034 . Arhivat (PDF) din original pe 2021-05-09 . Preluat 2021-03-24 . Parametrul depreciat folosit |deadlink=( ajutor )
↑ Asociația Europeană pentru Informatică Teoretică 2016 Premiul Gödel Arhivat 14 iulie 2016 la Wayback Machine
↑ Ynot . Consultat la 19 noiembrie 2014. Arhivat din original pe 25 februarie 2009. (nedefinit)
↑ Prădători . Data accesului: 19 noiembrie 2014. Arhivat din original pe 25 octombrie 2014. (nedefinit)
↑ Mutilin V.S., Novikov E.M., Khoroshilov A.V. Prezentare generală a instrumentelor pentru verificarea statică a programelor C aplicate driverelor de dispozitiv ale sistemului de operare Linux // Proceedings of the Institute for System Programming of the Russian Academy of Sciences. - 2012. - T. 22 , nr 3 . - S. 293-326 .
↑ Cliff Jones (de la U. Newcastle), Viktor Vafeiadis (de la MPI-SWS) Gândire bazată pe garanție și logică de separare Arhivat 29 noiembrie 2014 la Wayback Machine

Literatură

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. - P. 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, Zurich, Elveția, 10-13 octombrie 2005, Revised Selected Papers and Discussions / B. Meyer , J. Woodcock - Berlin : Springer Berlin Heidelberg , 2008. - P. 460-469. - ( Note de curs în Informatică ; 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 (engleză) // POPL '05 : Proceedings of the 32th ACM SIGPLAN-SIGACT simpozion on Principles of programming languages Long Beach, CA, SUA 12-14 ianuarie 2005 — Nou York , NY, SUA : ACM , 2005. - P. 247-258. - ISBN 978-1-58113-830-6 - doi:10.1145/1040305.1040326
Lee, Wonyeol și Park, Sungwoo. A Proof System for Separation Logic with Magic Wand (engleză) // SIGPLAN Not .. - ACM, 2014. - Vol. 49 , nr. 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 (engleză) - Cambridge University Press , 2014. - 472 p. — ISBN 978-1-107-04801-0
Ilya Serghei. 8.2 Bazele logicii separării // Programe și dovezi: Mecanizarea matematicii cu tipuri dependente . - 2014. - (Note de curs).
Peter W. O'Hearn. Un primer despre logica separării (și verificarea și analiza automată a programelor) // Siguranța și securitatea software-ului; Instrumente de analiză și verificare. - 2012. - Vol. 33. - P. 286-318.

Link -uri

Cliff Jones ( Newcastle University ), Viktor Vafeiadis ( MPI-SWS ) Rely-garantee thinking & separation logic (ing.) - prezentare care ilustrează bine conceptele de logica de separare
Matthew Parkinson An Introduction to Separation Logic (engleză) - o prezentare în care sunt ilustrate toate aspectele principale ale logicii separării: axiome, exemple de program cu diagrame corespunzătoare, sintaxă