FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:     | 1 |   ...   | 4 | 5 || 7 | 8 |   ...   | 22 |

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

-- [ Page 6 ] --

ii. In line 2, the program allocates and initializes a 4-word block of memory5. The local variable i is initialzied to 0 in line 3.

iii. In line 4, the bookkeeping instruction make lock turns memory location L from a normal memory location into a lock with an invariant R(L); see figure 3.2 for a schematic of the invariant. Informally, the invariant says that the lock L guards the next three locations in memory. The first two locations contain data values which are supposed to be equal. The last location contains a “continue” flag; a 1 indicates that the child thread is still computing, whereas a 0 indicates that it has completed. In section 4.9 we will formally discuss the exact invariant used. Like all locks, the lock is created in the locked state.

iv. In line 5, the function f is spawned as a child thread, and is passed the parameter L, the address of the still-locked lock.

v. In line 6, the continue field is set to 1, meaning that the child has not finished computing. Even though the child has already been started, this is safe because the child is not able to see the In the implemented Concurrent C minor, memory is byte-addressed; locks are word-sized and must be word-aligned. We simplify the presentation by assuming word addressing.


 continue field until it grabs the lock L, which is currently being held by the parent.

vi. In lines 7–13, the main thread loops. First, in line 8, it checks to see whether the continue flag has been reset to 0; if so, it breaks out of the loop. Then, in line 9, it modifies the data cells by setting them equal to the local variable i, before unlocking the lock in line 10. Then it increments i in line 11, grabs the lock again in line 12, and loops back around.

vii. Control reaches line 14 after the child process has set the continue flag to 0, indicating that it has completed. Accordingly, it should be safe to convert the location L from a lock back into a regular piece of memory, so we use the bookkeeping instruction free lock.

viii. In lines 15–16, there is a test that checks whether the two data cells contain the same value; if they do not, then the program gets stuck. Since both threads write to both data cells, it is not obvious whether this test will succeed. However, lines 9 and 24– 25, where the data fields are mutated, shows that as long as as the values are identical before they are modified, they will be identical afterwards. Since they both start as 0, we can informally conclude that they will be equal at this point in the program. In 4.9.2 we will formally prove that they are equal.

–  –  –

x. Line 21 declares the child process f. The precondition of the function f is that the argument l is a lock with invariant R(l), while the postcondition emp indicates that when the child terminates it will have given up all of its resources (including the lock passed as an argument).

xi. In lines 22–29, the child loops. It grabs the lock on line 23, and then modifies the protected data in lines 24–25. On line 26, the child tests to see if the first data cell is larger than 10; if so, it sets the continue flag to 0 in line 27, unlocks the lock in line 28, and exits the thread by returning from the function in line 29.

Otherwise, the thread unlocks the lock in line 31, and loops back around.

The explanation given above indicates what the example program does and why it is correct. In section 4.9 we give parts of the formal proof of correctness. Mansky provides a fully systematic proof of correctness in Coq using our Concurrent Separation Logic in [Man08].

Chapter 4

Concurrent Separation Logic

Concurrent Separation Logic for Concurrent C minor is a new program logic for reasoning about the correctness of programs written in Concurrent C minor. Here we present the assertions of the logic, give the Hoare rules using those assertions to reason about the concurrent language features, and demonstrate the power of the system by verifying the example program presented in section 3.2. The semantics of assertions and the Hoare tuple are quite complicated and so are deferred until chapters 7 and 10, respectively1.

–  –  –

To support reasoning in Concurrent Separation Logic, we have many of the usual assertions of Hoare logic: true and false; conjunction ∧ and disjunction ∨; universal and existential quantifiers ∀ and ∃; equirePortions of this chapter have been published before as [HAZ08a] and [HAZ08b].



 cursive assertions µF ; assertions in the base (Coq) logic [A]Coq ; and assertions that a C minor expression e evaluates to a value v, e ⇓ v. C minor expressions can read the heap but not write to it. Most of our separation logic operators take only pure expressions, i.e., those that do not read the heap. Appel and Blazy [AB07, §4] show how to bridge the pure-impure gap in Separation Logic by local program transformations.

We support impredicative quantification—that is, our universal and existential quantifiers range over all types, including assertions themselves. This powerful form of quantification is useful for reasoning about complex language features such as objects, higher-order functional programs, and generics.

We do not expose full implication to the user, since it interacts complexly with the underlying model. We do support many kinds of limited implication, however. Similarily, we do not expose full negation.

The problems surrounding implication are explained in section 7.3.7.

4.2 Sequential separation logic assertions To these Hoare logic assertions we add the standard assertions of separation logic: the empty heap emp, which gives no permission to access memory; the singleton “maps-to” e → v, which gives permission to access the location e, and asserts that location e currently contains the value v 2 ; and the separating conjunction P ∗ Q, which says that the Since C minor allows for variable-sized data, the actual relation used in the proofs also handles the size of the data, but this detail has been elided for the

4.3. FRACTIONAL OWNERSHIP  memory can be divided (not necessarily uniquely) into two parts, the first of which satisfies P and the second of which satisfies Q. We augment the maps-to assertion with the concept of fractional ownership.

4.3 Fractional ownership First-class locks are only useful if more than one thread has the ability to try to grab the lock at the same time. Fractional ownership allows the the ownership of an address to be split into pieces. With partial ownership of a standard location, reading from that location is allowed but writing to it is not. With partial ownership of a lock location, trying to acquire the lock is allowed.

Fractional ownerships also enable the verification of concurrent algorithms that utilize a multiple-reader, single-writer protocol; moreover, they can also simplify sequential reasoning. For example, at a function call, a caller can pass just the read permission for an address to the callee. After the callee returns, the caller will know that the callee did not modify the address (but could have read it)3.

–  –  –



Further applications of fractional ownership can be found in Boyland [Boy03] and Bornat et al. [BCOP05].


 Shares come with a join relation π1 ⊕ π2 = π, which indicates that the shares π1 and π2 combine to form the new share π. Not every pair of shares π1 and π2 join—often there is no π that will serve. We write πa ⊥ πb to mean that πa and πb join; that is, ∃πc. πa ⊕ πb = πc.

Conversely, we write πa ⊥ πb to mean that πa and πb do not join; that is, πa ⊥ πb ≡ ¬ (πa ⊥ πb ). We write πa ⊂ πc to mean that πa joins with some other share πb to equal πc ; that is, πa ⊂ πc ≡ ∃πb. πa ⊕ πb = πc.

4.4 Stratified separation algebras Our shares and the join relation are similar to the notion of a separation algebra as defined by Calcagno et al. [COY07]. A separation algebra is a partial commutative monoid with a cancellation property. That is, a

separation algebra has the following properties:

1. Determinism: (πa ⊕ πb = π1 ) ⇒ (πa ⊕ πb = π2 ) ⇒ π1 = π2

2. Associativity: (π1 ⊕ π2 = πa ) ⇒ (πa ⊕ π3 = π) ⇒

–  –  –

3. Commutativity: (π1 ⊕ π2 = π) ⇒ (π2 ⊕ π1 = π)

4. Cancellation: (π1 ⊕ πa = π) ⇒ (π2 ⊕ πa = π) ⇒ π1 = π2

5. Identity: ∃πe. ∀π. πe ⊕ π = π (1)–(5) gives a clean, standard definition, and it is possible to develop a model for shares with it (the identity is the empty share). However,

4.4. STRATIFIED SEPARATION ALGEBRAS  it will not be sufficient when the join relation is extened to resource maps in chapter 7, since the model presented there has multiple distinct empty resource maps. From an engineering perspective the generalization to multiple identity elements is simpler if it is done uniformly, since it means a lemma library needs to be developed only once. Accordingly,

we replace (5) with (6), which swaps the order of the quantifiers:

6. Multiple identities: ∀π. ∃πe(π). πe(π) ⊕ π = π The idea of multiple identity elements in a commutative setting is unusual, since there is a standard proof that in such a setting, if two identity elements join with each other then they must be equal.

Lemma 4.1.

If πe1 and πe2 are identity elements, and if

–  –  –

Proof. πe1 ⊥πe2 means that there exists π such that πe1 ⊕ πe2 = π. Since πe1 is an identity, we know that πe1 ⊕ πe2 = πe2. By cancellation, π = πe2. By commutativity, we know πe2 ⊕ πe1 = π. Since πe2 is an identity, πe2 ⊕ πe1 = πe1. By cancellation, we know that π = πe1. Thus, by transitivity of equality, πe1 = πe2. Proved in Coq.

However, join is a partial function, which means that not every element must join with a given identity. Therefore, it is reasonable to imagine a set of identity elements, each of which can join with certain other elements. Since if two identity elements join they must be the same


 element, this means that the sets of elements that join to particular empty elements form an equivalence class.

–  –  –

One additional property that we want for our join relation is

7. Split identities: ∀πa, πb, πe. (πa ⊕ πb = πe ) ⇒ identity πe ⇒ identity πa This property says that if two elements join to an identity element, then both must be an identity element as well; it is a kind of monotonicity property. Property (7) is not true for all separation algebras (e.g., Z with addition); however, it is true for common examples of separation algebras (e.g., sets of N with the disjoint union operation), and does not

4.5. ADDITIONAL PROPERTIES FOR SHARES  pose serious difficulties in a model. Accordingly, for us, a join relation has properties (1)–(4) and (6)–(7); it is a separation algebra with the pathological4 combination of multiple and split identities, which we call a stratified separation algebra 5. We call a type with a join relation that obeys the stratified separation algebra axioms a joinable type. Our Coq development has many different examples of joinable types.

4.5 Additional properties for shares A share and its join operation must satisfy the properties of a joinable type from section 4.4. In addition a share must have some additional

properties that are not always true for all separation algebras or separation logics:

8. Nonoverlapping: ∀πa, πb, πc. (πa ⊕ πb = πc ) ⇒ ¬identity πa ⇒

–  –  –

9. Splittability: there is a named total function split, which takes a

share and returns a pair of shares, and obeys the following rule:

–  –  –

These axioms are provided so that the user of CSL is able to develop more modular proofs. Property (8) gives the user a finer ability to distinguish shares from one another6. Property (9) allows the user to develop proofs of modules without the need to handle a share that cannot be further split. Property (10), illustrated in the diagram above, guarantees a more subtle kind of splitting, and helps the user develop more modular proofs.

Properties (8)–(10) could probably be included in the definition of a joinable type instead of being guaranteed only for shares7. However, shares have two fundemental properties that distinguish them from

other joinable types:

11. Full share: ∃πf. ∀π. π ⊂ πf

12. Nontrivial: ∃π. ¬identity π The usefulness of this ability is discussed in section 4.6. Property (8) is similar in some ways to property (7) in that both in some sense constrain the existance of inverses, but the precise relationship of property (7) to property (8) is not fully clear.

That (8)–(10) are defined only for shares, while (7) is defined for all joinable types could very well be historical accident relating to how the proof was developed;

for some future work it might be useful to determine whether (8)–(10) should be moved to joinable, or perhaps whether (7) should be moved to shares.

4.6. SHARE MODELS  Property (11) implies that shares have a partial order, with a (unique) top element, the full share. The partial ordering also guarantees the existence of a unique bottom element, the empty share8. Finally, property (12) guarantees that the system is nontrivial and completes the axiomitization. Accordingly, in our system, shares have properties (1)–(4) and (6)–(12)9.

Lifting joinability from shares to assertions. Given the above properties for shares, we can model the separating conjunction as a join relation in a more general way than Appel and Blazy. Two mapsπ π to assertions e → v and e → v separate if and only if π1 ⊥ π2. Two maps-to assertions about different locations always join. The assertion emp is the identity element.

Pages:     | 1 |   ...   | 4 | 5 || 7 | 8 |   ...   | 22 |

Similar works:

«TELOMERE DYNAMICS AND TELOMERASE-INDEPENDENT CELL SURVIVAL IN Arabidopsis thaliana A Dissertation by JAMES MATTHEW WATSON Submitted to the Office of Graduate Studies of Texas A&M University in partial fulfillment of the requirements for the degree DOCTOR OF PHILOSOPHY May 2007 Major Subject: Biochemistry TELOMERE DYNAMICS AND TELOMERASE-INDEPENDENT CELL SURVIVAL IN Arabidopsis thaliana A Dissertation by JAMES MATTHEW WATSON Submitted to the Office of Graduate Studies of Texas A&M University in...»

«Activated atmosphere case hardening of steels by Xiaolan Wang A Dissertation Submitted to the Faculty of the WORCESTER POLYTECHNIC INSTITUTE in partial fulfillment of the requirements for the Degree of Doctor of Philosophy in Material Science and Engineering Dec 2011 Approved: _ Prof. Richard D. Sisson Jr, Advisor Mr. Zbigniew Zurecki, Co-advisor Prof. Diran Apelian, Committee Member Prof., Makhlouf M. Makhlouf, Committee Member Prof. Jianyu Liang, Committee Member i ACKNOWLEDGMENTS I would...»


«Philosophy and Phenomenological Research Philosophy and Phenomenological Research Vol. LXXX No. 1, January 2010 Ó 2010 Philosophy and Phenomenological Research, LLC Introspection: Divided and Partly Eliminated peter carruthers University of Maryland This paper will argue that there is no such thing as introspective access to judgments and decisions. It won’t challenge the existence of introspective access to perceptual and imagistic states, nor to emotional feelings and bodily sensations. On...»

«DYNAMIC RESOURCE MANAGEMENT IN RESOURCE-OVERBOOKED CLOUD DATA CENTERS By Faruk Caglar Dissertation Submitted to the Faculty of the Graduate School of Vanderbilt University in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY in Computer Science August, 2015 Nashville, Tennessee Approved: Dr. Aniruddha S. Gokhale Dr. Douglas C. Schmidt Dr. Gautam Biswas Dr. Christopher J. White Dr. Akos Ledeczi To my beloved wife Fatma for her patience, encouragement, and support...»

«Living in the Moment: Boredom and the Meaning of Existence in Heidegger and Pessoa Jan Slaby Freie Universität Berlin jan.slaby@fu-berlin.de To appear in: Yearbook for Eastern and Western Philosophy, vol. 2, ed. by Hans Feger, Xie Dikun and Wang Ge, Berlin/New York: de Gruyter 2017. ABSTRACT Not only in his infamous speeches as NSDAP-approved Führer-Rektor of Freiburg University, Heidegger advocated what can seem like an ‘activist’ understanding of human existence. To exist, according to...»

«THE UNIVERSITY OF CHICAGO SOUTHERll BACKWOODS DICTION 18t9-1840 DISSERTATION A SUBMITTED TO THE GRADUATE FACULTY IU CANDIDACY FOR THE DEGREE OF DOCTOR OF PHILOSOPHY DEPARTMENT OF ENGLISH LANGUAGE LI TERATURE AND BY MITFORD McLEOD MATHEWS ILLIUOIS CHICAGO, JUNE, Introduction. From the time of John Witherspoon (1723-1794) there has been in this country more than a little interest in American English as distinguished from the English of England. In 1781 when Witherspoon wrote his articles dealing...»

«Lecture 4: Quantifiers and Monotonicity Jakub Szymanik Outline Monotone Quantifiers Monotonicity and Reasoning Monotonicity and Negativity Confound Sentence-picture Verification Models Experimental Hypotheses Based on Counting Experiments Results Discussion Monotonicity – Key Property in Logic and Language We saw that many factors influence verification. In this lecture we study another aspect: monotonicity. Important in logic, linguistics, learnability,... Hypothesis NL determiners...»

«Predictive Coding: How the Human Brain Uses Context to Facilitate the Perception of Degraded Speech By Conor James Wild A thesis submitted to the Centre for Neuroscience Studies in conformity with the requirements for the degree of Doctor of Philosophy Queen’s University Kingston, Ontario, Canada August, 2012 Copyright © Conor J. Wild, 2012 Abstract The most common and natural human behaviours are often the most computationally difficult to understand. This is especially true of spoken...»

«Corinna Lüthje, University of Hamburg Conceptualizing the interconnected agents of collective memory: The transforming perception of a regional geohazard between mediated discourse and conversation Paper presented to the ECREA Philosophy of Communication Conference “Landmarks2 – Communication and Memory”, 9.-11. Dez. 2009 in London Social memory is a constructive process rather than a fixed object, in which different actors constantly negotiate with each other in their respective...»

«EXPERIMENTAL INVESTIGATIONS OF PSEUDOSPARK DISCHARGE AND PSEUDOSPARK PRODUCED INTENSE ELECTRON BEAMS by JING HU A DISSERTATION Presented to the Faculty of the Graduate School of the MISSOURI UNIVERSITY OF SCIENCE AND TECHNOLOGY In Partial Fulfillment of the Requirements for the Degree DOCTOR OF PHILOSOPHY in AEROSPACE ENGINEERING Approved by Joshua L. Rovey, Advisor Kakkattukuzhy M. Isaac, David W. Riggins, Scott M. Kovaleski Carlos H. Castano  2012 Jing Hu All Rights Reserved iii...»

«Madhyamaka is Not Nihilism Jay L Garfield Smith College University of Melbourne Central University of Tibetan Studies Introduction Ngrjuna (c. 200 CE) is the founder of the Madhyamaka school of Buddhist philosophy, and easily, after the Buddha himself, the most influential philosopher in the Mahyna Buddhist tradition. Despite the great consensus on his philosophical and doctrinal importance, there is little consensus, either in the canonical Buddhist and non-Buddhist literature of...»

<<  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.