WWW.DISSERTATION.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Dissertations, online materials
 
<< HOME
CONTACTS



Pages:     | 1 |   ...   | 10 | 11 || 13 | 14 |   ...   | 22 |

«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»

-- [ Page 12 ] --

Using this partial function, one defines the oracular step with three cases as given in figure 6.10. The first case covers the situation when the core semantics is stepping. The second case covers when the oracle is taking control for an extended statement, but eventually returning control to the core. The third case is for when the extension does not return control to the core semantics, and therefore the program enters an infinite loop. For our work, the third case is only used when a deadlock occurs during the execution of a lock statement.

Chapter 7 A Modal Substructural Logic In chapter 4 we defined Concurrent Separation Logic, and in sections 6.2.1–6.2.2 we axiomatized resource and rmap and explained that the assertions of CSL were modeled as predicates.

In section 7.1 we explain the difficulties in providing a model for CSL assertions. In section 7.2 we explain the stratification technique that allows us to provide a sound definition for resources and resource maps. Finally, in section 7.3 we explain how to use a modal logic to reason cleanly about the underlying model and define the assertions of CSL1.

Portions of this chapter have been published before as [HAZ08a], [HAZ08b], [DAH08], and [BDH+ 08].

–  –  –

7.1 Modelling difficulties In section 6.2.1 we explained that a predicate is a function from a tuple of globals, locals, resource map, and memory to a proposition in the Calculus of Co-Inductive Constructions (Coq’s Prop). Though the ability to judge globals is important for developing proofs in CSL, modeling assertions about them is not difficult, so for the rest of this chapter, we elide globals to simplify the presentation; we also elide issues related to the C minor memory model outlined in section 6.3.2.

In section 6.2.1, it was also explained that neither resource maps nor memories depend on the syntax of programs and so can be used with any CompCert language, which further justifies using them whenever possible to express invariants in the soundness proof.

7.1.1 Semantic vs. Syntactic There are two basic approaches to programming language research. The first, more common today, is syntactic, where objects are uninterpreted symbols and are defined by judgements showing how they are to be used. The second, which is the approach we have taken, is semantic, where objects are given formal definitions and judgements showing how they should be used are proved from those definitions as lemmas.

We initially chose to give a semantic definition for our separation logic—instead of defining it syntactically and proving soundness via metaproofs—for three reasons. First, semantic systems are more exMODELLING DIFFICULTIES  tensible than syntactic ones. It is easy to define a new assertion, and unless the underlying semantics of the language must be changed to accomodate that assertion, all of the previously proved facts still hold automatically. Therefore in section 6.2.1 we were able to give a subset of the assertions of our CSL, including “maps-to” e → v and “is a lock π with invariant R” e ; R, without worrying that we were leaving anything out. If a user decides we have left out a useful assertion, he can define it himself.

Second, after examining the Princeton Foundational Proof-Carrying Code (FPCC) project [App01] we found evidence that semantic methods scaled better than syntactic ones in large, machine-checked, realistic systems [BDH+ 08].

Third, we had more experience with semantic methods in the context of a large project. Partially as a result of this experience, we find semantic proofs more natural than syntactic ones, and easier to construct.

Fourth, although we do not have any hard evidence for this opinion, we believe that semantic methods are less brittle than syntactic proofs when confronted with the kinds of engineering changes common in a large project.

–  –  –

The recursive nature of first-class locks makes them very difficult to model semantically since it is easy to slip into Cantor’s paradox. We

CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC



–  –  –

want a model that is something like the one in figure 7.1, where + and × are the sum and product type constructors and we write ≈ to mean “we wish we could define things this way”.

The idea is that a resource can either be NO, which indicates that the location cannot be used, or YES, which indicates that the resource can be used in some way. A YES resource takes a kind, which can be one of three choices: kVAL, which indicates that the location contains data; kLK, which indicates that the location is a lock; and kFUN, which indicates that the location contains a function. A YES resource also takes an pshare and list(predicate). As explained in section 6.2.2, a pshare is a nonempty share as defined in section 4.5. The “high-level” resource pseudoconstructors VAL, LK, and FUN are defined in terms of YES.

An rmap associates every location in memory with a resource. As explained in section 6.2.1, locals, rmap, and mem are bundled together into a world. A predicate then is a function from world to Prop.

–  –  –

In both cases, there is a contravariant occurrence of resource within its own definition. In other words, the cardinality of resource is strictly larger than the cardinality of resource, a contradiction even in untyped set theory. Thus these definitions are unsound.





7.1.3 From mutable references to lock invariants To provide a sound definition we adapt techniques developed for modeling mutable references in the FPCC project [AAV03, Ahm04]. It was surprising to us that the semantics of mutable references were relevant to the semantics of first-class locks. However, reading from a mutable reference is similar to locking a lock, in the sense that both actions are a way of getting information from the outside world. Analogously, storing to a mutable reference is similar to unlocking a lock, in the sense that both actions are a way of notifying the outside world of a change of state.

The indexed model developed for modelling mutable references in FPCC was extremely difficult to explain and very complex to use. It was developed in higher-order logic (HOL) encoded in the Twelf theorem prover; limitations on the expressiveness of HOL required extensive, very heavyweight G¨delization techniques to define the model and prove o it sound, resulting in more than 20,000 lines of proof for this part of the model alone. Also, the underlying model was exposed to the rest of the proof of the type system in various unpleasant ways.

–  –  –

to create a modal model. This model was defined and proved sound in Coq in approximately 1,000 lines. The enormous difference in size is due to a combination of several factors: first, substantial redesign of the definitions and better proof techniques; second, the natural difference

–  –  –

7.2 A substructural modal model The sketch of the modal substructural model given in figure 7.2 is divided into three parts. The first section shows how we provide a sound definition in the presence of contravariance in a way that preserves impredicativity. The second section shows how dependent types can hide the stratification in the underlying model. The third section gives some definitions that are useful when translating the dependent model into the underlying stratified model2.

–  –  –

◦ model. We use = to mean that the definition is opaque to the rest of For further details of the stratification and soundness of the construction we refer to Appel et al. [AMRV07] and Richards [Ric08]; both refer to the 1,000 line Coq development cited earlier. Appel [App08] has also illustrated some of the modifications required to support substructural reasoning.

CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC



–  –  –

the proof; that is, the rest of the proof knows that the definition exists, but is not able to “look inside” and see the details of the definition. We use = to mean that the definition is completely public, and that the rest of the proof is able to use it directly.

There are a number of differences between the presentation here

and the Coq development. The most important ones are these:

1. Here predicates judge only locals, resource maps, and memory;

as explained in section 6.2.1, in the Coq development, predicates also judge globals.

2. Here we ignore issues related to byte addressability. In the Coq development, we must handle this issue. In particular, we need to ensure that the first byte of a lock cannot be separated from the following three bytes. We do this by maintaining validity predicates about valid resource maps.

3. As explained in section 4.7.3, in the presentation we do not support the relation of function preconditions to function postconditions; i.e., we do not have a way of expressing that a call to an increment function returns a value exactly one larger than its parameter. In the actual Coq development, both our CSL and the underlying model support this additional expressiveness. In the model this is done by parameterizing predicate lists over an additional type and value parameter.

CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC



4. Here we use the → type constructor to construct the types of rmapn and rmap. In the Coq development we use a quasifunctor called Joinmap that helps preserve certain separation properties.

5. Our presentation here is less modular than the Coq development.

6. It is nontrivial to produce definitions that will be acceptable to the Coq theorem prover from the definitions as given in the presentation, largely due to the heavy use of dependent types in the model. In appendix A we give a very compact Coq development that implements the core ideas presented in figure 7.2; this miniature development should help a reader who wishes to understand (or build) a larger Coq implementation. In the real Coq development, the entire modal substructural model has been completely defined and proved sound.

7.2.1 An impredicative stratified model The idea is that we will stratify predicates, resources, and rmaps; we write predicaten to mean a predicate at level n, resourcen to mean a resource at level n, and rmapn to mean a resource map at level n.

To ensure a well-founded construction, we define predicate0 as unit.

A resource at level n is only allowed to contain predicates of level n;

similarly, a resource map at level n is a map from address to resourcen.

As discussed in section 6.2.1, we bundle locals, resourcen, and memory together into a worldn. A predicate at level n + 1 is a pair of predicaten

7.2. A SUBSTRUCTURAL MODAL MODEL  and a map from worldn to Prop. Thus, a predicate at level n+1 contains a list of predicates for all levels between n and 0, in addition to the map

from worldn to Prop. As an example, consider n = 3:

predicate3 = (unit × (world1 → Prop)) × (world2 → Prop).

We define predicaten as a pair because it lets us define “aging” the predicate in section 7.2.4 in a relatively simple way.

By stratifying in this manner we make the definitions well-defined.

The stratified construction was one of the major technical accomplishments of the indexed model for mutable references that Ahmed et. al [AAV03, Ahm04] developed for the FPCC project.

One major advantage of this construction over previous models [AM01, AAV02] is that it supports impredicative quantification. That is, since the result type of predicaten is Prop (as opposed to, e.g., some kind of stratified Propn ), it is possible to define universal and existential quantifiers for predicaten that can quantify over all of the types in Coq, even including predicaten. This is much stronger and more useful than predicative quantification, where a predicaten could at most quantify over predicaten−1.

One major drawback in the model developed for FPCC is that the

–  –  –

resourcen, worldn, and rmapn, indicating that the rest of the proof cannot see the underlying stratification.

7.2.2 Dependent types to hide stratification The second section in figure 7.2 contains one of the major insights in the modal model of Appel et. al [AMRV07], namely the ability to hid the underlying indexes in the model from the rest of the proof by using dependent types. Explicit reasoning about the indexes can therefore be contained to a small part of the overall soundness proof.

We use both sum (Σ) and product (Π) dependent types in our definitions. An element s : Σα. (β : α → Type) is a dependent pair, written s = {a : α, b : β(a)}, where the type of the second component depends on the value of the first component3.

An element f : Πα. (β : α → Type) is a dependent function f = λa : α.(b a) : β(a), where b : α → β(a). Thus, the type of the function’s result depends on the value of the function’s parameter. One way to interpret this is that the Π type operator defines a family of related types, indexed by the value.

Using the Σ dependent type constructor, we are able to define resource as a dependent pair of a natural n and a stratified resourcen at level n. Similarily, we define rmap as a dependent pair of a natural n and a stratified rmapn at level n. These definitions elegantly hide the underlying stratification by bundling it into a dependent pair, and are To express a normal pair we use the typical notation (a, b); the notation {a, b} is reserved to indicate the presence of dependent types.

7.2. A SUBSTRUCTURAL MODAL MODEL  the definitions axiomatized in section 6.2.2. Finally, predicate is defined as was promised in section 6.2.1, as a function from a pair of rmap and mem to Prop.



Pages:     | 1 |   ...   | 10 | 11 || 13 | 14 |   ...   | 22 |


Similar works:

«Ecosystem Spatial Heterogeneity: Formation, Consequences, and Feedbacks by Xiaoli Dong A Dissertation Presented in Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy Approved August 2015 by the Graduate Supervisory Committee: Nancy Grimm, Co-Chair Rachata Muneepeerakul, Co-Chair Janet Franklin James Heffernan John Sabo ARIZONA STATE UNIVERSITY December 2015 ABSTRACT An understanding of the formation of spatial heterogeneity is important because spatial heterogeneity...»

«Selectively De-animating and Stabilizing Videos by Jiamin Bai A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in Computer Science in the Graduate Division of the University of California, Berkeley Committee in charge: Professor Ravi Ramamoorthi, Chair Professor Maneesh Agarwala Professor Marty Banks Fall 2014 Selectively De-animating and Stabilizing Videos Copyright 2014 by Jiamin Bai 1 Abstract Selectively De-animating and Stabilizing...»

«Behavioral Correlates of Hippocampal Neural Sequences Anoopum S. Gupta CMU-RI-TR-11-36 Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Robotics The Robotics Institute School of Computer Science Carnegie Mellon University Pittsburgh, Pennsylvania 15213 September 2011 Thesis Committee David S. Touretzky (Chair) Tai Sing Lee Reid Simmons George Stetten A. David Redish, University of Minnesota Copyright c 2011 by Anoopum S. Gupta. All rights reserved....»

«NOT NOTHINGNESS: PETER BROOK’S ‘EMPTY SPACE’ AND ITS ARCHITECTURE Negin Djavaherian School of Architecture McGill University, Montreal, Canada August 2012 A thesis submitted to McGill University in partial fulfilment of the requirements of degree of Doctor of Philosophy © Negin Djavaherian, 2012 To my parents, Parvaneh and Hassan, and to Alois ABSTRACT The thesis explores architectural potential and experience in the theatre of Peter Brook (1925-). The importance of his thought, writings...»

«NORTHWESTERN UNIVERSITY Toward Rotational Cooling of Trapped SiO+ by Optical Pumping A DISSERTATION SUBMITTED TO THE GRADUATE SCHOOL IN PARTIAL FULFILLMENT OF THE REQUIREMENTS for the degree DOCTOR OF PHILOSOPHY Field of Physics and Astronomy By David Tabor EVANSTON, ILLINOIS June 2014 UMI Number: 3627205 All rights reserved INFORMATION TO ALL USERS The quality of this reproduction is dependent upon the quality of the copy submitted. In the unlikely event that the author did not send a complete...»

«Investigations into the Optically Stimulated Luminescence Response of Various Materials by William Geoffrey West A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Nuclear Engineering and Radiological Sciences) in the University of Michigan 2011 Doctoral Committee: Professor Kimberlee J. Kearfott, Chair Professor Rodney C. Ewing Professor Ronald M. Gilgenbach Professor Zhong He Joseph A. Miklos © William Geoffrey West 2011 For Dad ii...»

«Moral Concepts And Theories (ESSAY #3) Introduction In considering issues in engineering ethics, a distinction is sometimes made between morals and ethics. When this distinction is made, the term morals is taken to refer to generally accepted standards of right and wrong in a society and the term ethics is taken to refer to more Abstract principles which might appear in a code of professional ethics or in a textbook in ethical theory. However, the terms moral philosophy or moral theory would...»

«Leveraging Light-Weight Analyses to Aid Software Maintenance A Dissertation Presented to the Faculty of the School of Engineering and Applied Science University of Virginia In Partial Fulfillment of the requirements for the Degree Doctor of Philosophy (Computer Science) by Zachary P. Fry May 2014 c 2014 Zachary P. Fry Abstract While software systems have become a fundamental part of modern life, they require maintenance to continually function properly and to adapt to potential environment...»

«Multiple System Atrophy and Parkinson’s disease Thesis submitted for the degree doctor of philosophy By Haya Kisos Submitted for the senate of Hebrew University June 2013 This work was carried out by supervision of Dr. Ronit Sharon and Prof. Tamir Ben Hur Abstract: The synucleinopathies are a diverse group of neurodegenerative disorders that share a common pathologic intracellular lesion, composed primarily of aggregates of insoluble α-Synuclein (α-Syn) protein in selectively vulnerable...»

«INTERACTIVE SIMULATION OF FIRE, BURN AND DECOMPOSITION A Dissertation by ZEKI MELEK Submitted to the Office of Graduate Studies of Texas A&M University in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY December 2007 Major Subject: Computer Science INTERACTIVE SIMULATION OF FIRE, BURN AND DECOMPOSITION A Dissertation by ZEKI MELEK Submitted to the Office of Graduate Studies of Texas A&M University in partial fulfillment of the requirements for the degree of...»

«OREGON STATE UN VERS TY LIBRARIES 1111 1111 11 11111 1111 12 0003896558 Tillamook Prehistory and Its Relation to the Northwest Coast Culture Area by Thomas M. Newman /-iPARTMENT OF ANTHROPfottLIBRARY, TILLAMOOK PREHISTORY AND ITS RELATION TO THE NORTHWEST COAST CULTURE AREA by THOMAS M. NEWMAN A THESIS Presented to the Department of Anthropology and the Graduate School of the University of Oregon in partial fulfillment of the requirements for the degree of Doctor of Philosophy June 1959...»

«UNIVERSITY OF CALIFORNIA, SAN DIEGO Efficient Thermal Management for Multiprocessor Systems A dissertation submitted in partial satisfaction of the requirements for the degree Doctor of Philosophy in Computer Science and Engineering by Ay¸e Kıvılcım Co¸kun s s Committee in charge: ˘ Tajana Simuni´ Rosing, Chair c Kenny C. Gross Rajesh Gupta Tara Javidi Andrew B. Kahng Dean Tullsen 2009 Copyright Ay¸e Kıvılcım Co¸kun, 2009 s s All rights reserved. The dissertation of Ay¸e...»





 
<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.