programs that manipulate pointer data structures—including information hiding in the presence of pointers;
"transfer of ownership" (avoidance of semantic frame axioms); and
virtual separation (modular reasoning) between concurrent modules.
Separation logic supports the developing field of research described by Peter O'Hearn and others as local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include automated program verification (where an algorithm checks the validity of another algorithm) and automated parallelization of software.
Assertions: operators and semantics
Separation logic assertions describe "states" consisting of a store and a heap, roughly corresponding to the state of local (or stack-allocated) variables and dynamically-allocated objects in common programming languages such as C and Java. A store is a function mapping variables to values. A heap is a partial function mapping memory addresses to values. Two heaps and are disjoint (denoted ) if their domains do not overlap (i.e., for every memory address , at least one of and is undefined).
The logic allows to prove judgements of the form , where is a store, is a heap, and is an assertion over the given store and heap. Separation logic assertions (denoted as , , ) contain the standard boolean connectives and, in addition, , , , and , where and are expressions.
The constant asserts that the heap is empty, i.e., when is undefined for all addresses.
The binary operator takes an address and a value and asserts that the heap is defined at exactly one location, mapping the given address to the given value. I.e., when (where denotes the value of expression evaluated in store ) and is otherwise undefined.
The binary operator (pronounced star or separating conjunction) asserts that the heap can be split into two disjoint parts where its two arguments hold, respectively. I.e., when there exist such that and and and .
The binary operator (pronounced magic wand or separating implication) asserts that extending the heap with a disjoint part that satisfies its first argument results in a heap that satisfies its second argument. I.e,. when for every heap such that , also holds.
The operators and share some properties with the classical conjunction and implication operators. They can be combined using an inference rule similar to modus ponens
and they form an adjunction, i.e., if and only if for ; more precisely, the adjoint operators are and .
Reasoning about programs: triples and proof rules
In separation logic, Hoare triples have a slightly different meaning than in Hoare logic. The triple asserts that if the program executes from an initial state satisfying the precondition then the program will not go wrong (e.g., have undefined behaviour), and if it terminates, then the final state will satisfy the postcondition . In essence, during its execution, may access only memory locations whose existence is asserted in the precondition or that have been allocated by itself.
In addition to the standard rules from Hoare logic, separation logic supports the following very important rule:
This is known as the frame rule (named after the frame problem) and enables local reasoning. It says that a program that executes safely in a small state (satisfying ), can also execute in any bigger state (satisfying ) and that its execution will not affect the additional part of the state (and so will remain true in the postcondition). The side condition enforces this by specifying that none of the variables modified by occur free in , i.e. none of them are in the 'free variable' set of .
Sharing
Separation logic leads to simple proofs of pointer manipulation for data structures that exhibit regular sharing patterns which can be described simply using separating conjunctions; examples include singly and doubly linked lists and varieties of trees. Graphs and DAGs and other data structures with more general sharing
are more difficult for both formal and informal proof. Separation logic has, nonetheless, been applied successfully to reasoning about
programs with general sharing.
In their POPL'01 paper,[3] O'Hearn and Ishtiaq explained how the magic wand connective could be used to reason in the presence of sharing, at least in principle.
For example, in the triple
we obtain the weakest precondition for a statement that mutates the heap at location , and this works for any postcondition, not only one that is laid out neatly using the separating conjunction. This idea was taken much further by Yang, who used to provide localized reasoning about mutations in the classic Schorr-Waite graph marking algorithm.[8] Finally, one of the most recent works in this direction is that of Hobor and Villard,[9] who
employ not only but also a connective
which has variously been called overlapping conjunction or sepish,[10] and which can be used to describe overlapping data structures: holds of a heap when
and hold for subheaps and whose union is , but which possibly have a nonempty portion in common. Abstractly, can be seen to be a version of the fusion connective of relevance logic.
Concurrent separation logic
A Concurrent Separation Logic (CSL),
a version of separation logic for concurrent programs, was originally proposed by Peter O'Hearn,[11]
using a proof rule
which allows independent reasoning about threads that access separate storage. O'Hearn's proof rules adapted an early approach of Tony Hoare to reasoning about concurrency,[12]
replacing the use of scoping constraints to ensure separation by reasoning in separation logic. In addition to extending Hoare's approach to apply in the presence of heap-allocated pointers, O'Hearn showed how reasoning in concurrent separation logic could track dynamic ownership transfer of heap portions between processes; examples in the paper include a pointer-transferring buffer, and a memory manager.
Commenting on the early classical work on interference freedom by Susan Owicki and David Gries, O'Hearn says that explicit checking for non-interference isn't necessary because his system rules out interference in an implicit way, by the nature of the way proofs are constructed.
A model for concurrent separation logic was first provided by Stephen Brookes in a companion paper to O'Hearn's.[13] The soundness of the logic had been a difficult problem, and in fact a counterexample of John Reynolds had shown the unsoundness of an earlier, unpublished version of the logic; the issue raised by Reynolds's example is described briefly in O'Hearn's paper, and more thoroughly in Brookes's.
At first it appeared that CSL was well suited to what Dijkstra had called loosely connected processes,[14] but perhaps not to fine-grained concurrent algorithms with significant interference. However, gradually it was realized that the basic approach of CSL was considerably more powerful than first envisaged, if one employed non-standard models of the logical connectives and even the Hoare triples.
An abstract version of separation logic was proposed that works for Hoare triples
where the preconditions and postconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model.[15]
Later, by suitable choice of commutative monoid, it was surprisingly found that the proof rules of abstract versions of concurrent separation logic could be used to reason about interfering concurrent processes, for example by encoding the rely-guarantee technique which had been originally proposed to reason about interference;[16] in this work the elements of the model were considered not resources, but rather "views" of the program state, and a non-standard interpretation of Hoare triples accompanies the non-standard reading of pre and postconditions.
Finally, CSL-style principles have been used to compose reasoning about program histories instead of program states, in order to provide modular techniques for reasoning about fine-grained concurrent algorithms.[17]
Versions of CSL have been included in many interactive and semi-automatic (or "in-between") verification tools as described in the next section. A particularly significant verification effort is that of the μC/OS-II kernel mentioned there. But, although steps have been made,[18] as of yet CSL-style reasoning has been included in comparatively few
tools in the automatic program analysis category (and none mentioned in the next section).
O'Hearn and Brookes are co-recipients of the 2016 Gödel Prize for their invention of Concurrent Separation Logic.[19]
Verification and program analysis tools
Tools for reasoning about programs fall on a spectrum from fully automatic program analysis tools, which do not require any user input, to interactive tools where the human
is intimately involved in the proof process. Many such tools have been developed; the following list includes a few representatives in each category.
Automatic Program Analyses. These tools typically look for restricted classes of bugs (e.g., memory safety errors) or attempt to prove their absence, but fall short of proving full correctness.
A current example is Facebook Infer, a static analysis tool for Java, C, and Objective-C based on separation logic and bi-abduction.[20] As of 2015 hundreds of bugs per month were being found by Infer and fixed by developers before being shipped to Facebook's mobile apps[21]
Other examples include SpaceInvader (one of the first SL analyzers), Predator (which has won several verification competitions), MemCAD (which mixes shape and numerical properties) and SLAyer (from Microsoft Research, focussed on data structures found in device drivers)
Interactive Proof. Proofs have been done using embeddings of Separation Logic into interactive theorem provers such as the Coq proof assistant and HOL (proof assistant). In comparison to the program analysis work, these tools require more in the way of human effort but prove deeper properties, up to functional correctness.
A proof of the FSCQ file system[22] where the specification includes behaviour under crashes as well as normal operation. This work won the best paper award at the 2015 Symposium on Operating System Principles.
Verification of a large fragment of the Rust type system and some of its standard libraries in the RustBelt project using the Iris framework for separation logic in The Coq proof assistant.
Verification of an OpenSSL implementation of a cryptographic authentication algorithm,[23] utilizing verifiable C
Verification of key modules of a commercial OS kernel, the μC/OS-II kernel, the first commercial pre-emptive kernel to have been verified.[24]
In Between. Many tools require more user intervention than program analyses, in that they expect the user to input assertions such as pre/post specs for functions or loop invariants, but after this input is given they attempt to be fully or almost fully automatic; this mode of verification goes back to classic works in the 1970s such as J King's verifier, and the Stanford Pascal Verifier. This style of verifier has recently been called auto active verification, a term which intends to evoke the way of interacting with a verifier via an assert-check loop, analogous to the interaction between a programmer and a type-checker.
The very first Separation Logic verifier, Smallfoot, was in this in-between category. It required the user to input pre/post specs, loop invariants, and resource invariants for locks. It introduced a method of symbolic execution, as well as an automatic way to infer frame axioms. Smallfoot included Concurrent Separation Logic.
SmallfootRG is a verifier for a marriage of separation logic and the classic rely/guarantee method for concurrent programs.
VeriFast is an advanced current tool in the in-between category. It has demonstrated proofs ranging from object-oriented patterns to highly concurrent algorithms and to systems programs.
Viper is a state-of-the-art automated verification infrastructure for permission-based reasoning. It mainly consists of a programming language and two verification backends, one based on symbolic execution and another one on verification condition generation (VCG).[26] Based on the Viper infrastructure, several frontends for various programming languages have emerged: Gobra for Go, Nagini for Python, Prusti for Rust, and VerCors for C, Java, OpenCL, and OpenMP. These frontends translate the frontend programming language into Viper to then use a Viper verification backend for proving the input program's correctness.
The distinction between interactive and in-between verifiers is not a sharp one. For example,
Bedrock strives for a high degree of automation, in what it terms mostly-automatic verification, where
Verifast sometimes requires annotations that resemble the tactics (little programs) used in interactive verifiers.
Decidability and complexity
The satisfiability problem for a quantifier-free, multi-sorted fragment of separation logic parameterized over the sorts of locations and data can be shown to be PSPACE-complete.[27] An algorithm for solving this fragment in DPLL(T)-based SMT solvers has been integrated into cvc5.[28] Extending this result, satisfiability for an analog of the Bernays–Schönfinkel class for separation logic with uninterpreted memory locations can also be shown to be PSPACE-complete, whereas the problem is undecidable with interpreted memory locations (e.g., integers) or further quantifier alternations[29]
^Reynolds, John C. (1999). "Intuitionistic Reasoning about Shared Mutable Data Structure". In Davies, Jim; Roscoe, Bill; Woodcock, Jim (eds.). Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare. Palgrave.
العلاقات البحرينية الدومينيكية البحرين دومينيكا البحرين دومينيكا تعديل مصدري - تعديل العلاقات البحرينية الدومينيكية هي العلاقات الثنائية التي تجمع بين البحرين ودومينيكا.[1][2][3][4][5] مقارنة بين البلدين هذه مقارنة عامة ومرجعية للدولتي�...
1973 film by Robert Altman This article is about the 1973 Robert Altman film. For the 1982 Hong Kong film, see The Head Hunter. For the 2020 album, see The Long Goodbye (Riz Ahmed album). The Long GoodbyeTheatrical release posterDirected byRobert AltmanScreenplay byLeigh BrackettBased onThe Long Goodbyeby Raymond ChandlerProduced byJerry BickStarringElliott GouldNina van PallandtSterling HaydenCinematographyVilmos ZsigmondEdited byLou LombardoMusic byJohn WilliamsProductioncompanyLion's Gate ...
Disciple of Gautama Buddha This article is about a Buddhist bhikkhu. For other uses, see Yasa (disambiguation). Venerable YasaPersonalBorn6th century BCEVaranasi, IndiaReligionBuddhismOccupationbhikkhuSenior postingTeacherGautama Buddha Conversion of Yasa; a modern depiction in a Thai temple Part of a series onBuddhism Glossary Index Outline History Timeline The Buddha Pre-sectarian Buddhism Councils Silk Road transmission of Buddhism Decline in the Indian subcontinent Later Buddhists Buddhis...
Voce principale: Coppa UEFA 1989-1990. Finale della Coppa UEFA 1989-1990 Il portiere juventino Stefano Tacconi, nell'occasione capitano, solleva la seconda Coppa UEFA della storia bianconera. Dettagli evento Competizione Coppa UEFA Risultato Juventus3 Fiorentina1 Andata Juventus3 Fiorentina1 Data 2 maggio 1990 Città Torino Impianto di gioco Stadio Comunale Vittorio Pozzo Spettatori 47 519 Arbitro Emilio Soriano Aladrén Ritorno Fiorentina0 Juventus0 Data 16 maggio 1990 Citt...
У этого термина существуют и другие значения, см. Трезубец (значения). Запрос «Острога» перенаправляется сюда. На эту тему нужно создать отдельную статью. Скульптура Посейдона в Копенгагене Трезу́бец[1] (острога́[2] или «Нептунов жезл») — оружие, которое состоит...
Series of Israeli communications satellites Not to be confused with AMOS (satellite bus). AMOSModel of Israeli AMOS-5 satellite during Semana de Espacio, in IFEMA, Madrid.ManufacturerIsrael Aerospace Industries, ISS Reshetnev (AMOS-5)Country of originIsraelOperatorSpacecomApplicationsCommunications SpecificationsBusAMOS busEkspress bus (AMOS-5)Boeing 702 bus (AMOS-17)RegimeGeostationary ProductionStatusActiveBuilt7 knownLaunched5Operational3Failed1Lost1Maiden launchAMOS-1 - 16 May 1996Last la...
خوسف خوسف city الاسم الرسمي Khusf الإحداثيات 32°48′11″N 58°54′14″E / 32.80306°N 58.90389°E / 32.80306; 58.90389 تقسيم إداري الدولة إيران المحافظة خراسان جنوبي المقاطعة مقاطعة خوسف الناحية Central District عاصمة لـ مقاطعة خوسف خصائص جغرافية ارتفاع 1309 متر[1] عدد السكان...
Election in Sweden 1948 Swedish general election ← 1944 19 September 1948 1952 → All 230 seats in the Andra kammaren of the Riksdag116 seats needed for a majority First party Second party Third party Leader Tage Erlander Bertil Ohlin Axel Pehrsson-Bramstorp Party Social Democrats People's Party Farmers' League Last election 115 26 35 Seats won 112 57 30 Seat change 3 31 5 Popular vote 1,789,459 882,437 480,421 Percentage 46.1% 22.7% 12.4...
Lee Metcalf WildernessIUCN category Ib (wilderness area)Show map of the United StatesShow map of MontanaLocationMadison / Gallatin counties, Montana, USANearest cityBozeman, MTCoordinates45°08′N 111°27′W / 45.133°N 111.450°W / 45.133; -111.450Area254,288 acres (1,029.07 km2)Established1983Governing bodyU.S. Forest ServiceU.S. Bureau of Land Management The Lee Metcalf Wilderness is located in the northern Rocky Mountains in the U.S. state of Monta...
Town and municipality in Puerto Rico Town and Municipality in Puerto Rico, United StatesTrujillo Alto Municipio Autónomo de Trujillo AltoTown and MunicipalitySanta Cruz de TrujilloThe Loíza Lake and reservoir FlagCoat of armsNicknames: Ciudad de los Manantiales,El Pueblo de las Ocho Calles,La Ciudad En El Campo,Los ArrecostaosAnthem: Duerme Mi Lindo TrujilloMap of Puerto Rico highlighting Trujillo Alto MunicipalityCoordinates: 18°21′46″N 66°1′3″W / 18.36278°N...
スターダスト 著者ニール・ゲイマン原題Stardust翻訳者金原瑞人野沢佳織絵チャールズ・ヴェス(英語版)国 アメリカ合衆国言語英語ジャンルFantasy出版社DCコミックス角川文庫出版日2007年英語版出版日1999年出版形式Hardback, Paperback, Audiobook (Read by the author)ページ数256ISBN978-0-380-97728-4OCLC39313435 『スターダスト』(原題:Stardust)は、ニール・ゲイマンのファンタジー小説(�...
CNBC AfricaDiluncurkan1 Juni 2007PemilikAfrica Business News dan NBC UniversalSloganFirst In Business WorldwideKantor pusat Johannesburg, Afrika SelatanSitus webhttp://www.cnbcafrica.com/ Consumer News and Business Channel Africa (disingkat CNBC Africa) adalah layanan televisi untuk Sub-Sahara Afrika yang diluncurkan oleh CNBC. Dikontrol oleh Africa Business News Limited, saluran ini didirikan pada tanggal 1 Juni 2007.[1] Pada awalnya, CNBC Africa memiliki biro di Nairobi (Kenya), Abu...
Sieciech (lahir: abad ke-11 - wafat setelah tahun 1100) tokoh terkemuka dan negarawan abad pertengahan di Polandia. Biografi Gereja Santo Andrews di Kraków didirikan oleh Palatine Sieciech Seluruh informasi mengenai Sieciech telah diterbitkan dari penulis riwayat Gallus Anonymus. Ia merupakan seorang pangeran palatine di istana adipati Władysław I Herman Polandia. Meskipun tanggal kelahiran dan kematian yang sesungguhnya tidak diketahui, ia dikatakan oleh Gallus Anonymus tinggal di perteng...
Der Titel dieses Artikels ist mehrdeutig. Weitere Bedeutungen sind unter Baden-Baden (Begriffsklärung) aufgeführt. Wappen Deutschlandkarte Basisdaten Koordinaten: 48° 46′ N, 8° 14′ O48.7619444444448.2408333333333161Koordinaten: 48° 46′ N, 8° 14′ O Bundesland: Baden-Württemberg Regierungsbezirk: Karlsruhe Höhe: 161 m ü. NHN Fläche: 140,19 km2 Einwohner: 57.420 (31. Dez. 2023)[1] Bevölkerungsdichte:...
College of the University of Oxford Balliol CollegeUniversity of OxfordArms: Azure, a lion rampant argent, crowned or, impaling Gules, an orle argent[1] LocationBroad Street, Oxford, OX1 3BJCoordinates51°45′17″N 1°15′28″W / 51.7547°N 1.2578°W / 51.7547; -1.2578Full nameThe Master and Scholars of Balliol College in the U...
Voce principale: Supercoppa Primavera. Supercoppa Primavera 2009Supercoppa Primavera TIM 2009 Competizione Supercoppa Primavera Sport Calcio Edizione 6ª Organizzatore Lega Calcio Date 8 settembre 2009 Luogo Palermo Partecipanti 2 Formula Gara unica Impianto/i Stadio Renzo Barbera Risultati Vincitore Genoa(1º titolo) Secondo Palermo Statistiche Gol segnati 4 Lo Stadio Renzo Barbera di Palermo che ha ospitato la Supercoppa 2009. Cronologia della competizione 2008 2010 Manuale La ...
2012 American filmFar Out Isn't Far Enough: The Tomi Ungerer StoryOfficial PosterDirected byBrad BernsteinWritten byBrad BernsteinProduced byBrad Bernstein, Rick CikowskiStarringTomi Ungerer, Maurice Sendak, Jules Feiffer, Steven Heller, Michael Patrick HearnCinematographyJimmy O'DonnellEdited byRick Cikowski, Brandon Dumlao, Jason SchmidtMusic byBen Sollee, Eoin Coughlan & Daragh DukesProductioncompanyCorner of the Cave MediaDistributed byFirst Run FeaturesRelease dates July 5, ...
Wittes La mairie et le monument aux morts ;en arrière-plan, l'église Saint-Omer. Blason Administration Pays France Région Hauts-de-France Département Pas-de-Calais Arrondissement Saint-Omer Intercommunalité Communauté d'agglomération du Pays de Saint-Omer Maire Mandat Pascal Danvin 2020-2026 Code postal 62120 Code commune 62901 Démographie Gentilé Wittois Populationmunicipale 997 hab. (2021 ) Densité 254 hab./km2 Géographie Coordonnées 50° 40′ 13″...
Linguistic classification See also: Hammarström classification BantuNarrow BantuGeographicdistributionAfrica, from approximately the equator southLinguistic classificationNiger–Congo?Atlantic–CongoVolta-CongoBenue–CongoBantoidSouthern BantoidBantuSubdivisions Zones A–S (geographic) Language codesGlottolognarr1281The approximate locations of the sixteen Guthrie Bantu zones, including the addition of a zone J The 250 or so Narrow Bantu languages are conventionally divided up into geogr...
Army of the JamesThe Negro quarters of the Army of the JamesActiveApril 1864 – August 1865Country United States of AmericaBranch United States ArmyTypeField ArmyEngagementsAmerican Civil WarCommandersNotablecommandersBenjamin F. ButlerEdward OrdMilitary unit The Army of the James was a Union Army that was composed of units from the Department of Virginia and North Carolina and served along the James River during the final operations of the American Civil War in Virginia. History The Un...