FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:     | 1 |   ...   | 17 | 18 || 20 | 21 |   ...   | 22 |

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

-- [ Page 19 ] --

4. No support for nonlocal exits. As explained in chapter 2, C minor supports various kinds of nonlocal exits; to reason about these we add parameters R and B to the Hoare tuple. We omit them here since these features are directly related neither to concurrency nor to the core of our new definition of the Hoare tuple.

5. Miscellaneous. Other changes to improve the presentation.

–  –  –

We start with safeΨ κ, or predicate-level safe, which lifts the safe notion into the modal substructural logic by “hardcoding” the program Ψ and control κ into the predicate. If

–  –  –

then the control κ is safe with world w in the context of program Ψ.

Just as in the case of the simpler definitions, we define the notion of a predicate P guarding a control κ in the context of a program Ψ with P ⊓Ψ κ, or predicate-level guard. Recall from section 7.3.7 that ⊔ the predicate P ⊂ Q is a safe form of logical implication in the modal logic, informally equivalent to “On any world of equal or greater approximation than the current one, P implies Q”. Therefore

–  –  –

means that for any world w ′ with level less than or equal to the level of w, if w ′ |= P, then Ψ ⊢ safe (w ′, κ).

Our modal Hoare judgment takes a single argument of type Hargs, which is a tuple of predicate (Γ), predicate (P ), statement (c), and predicate (Q). We must uncurry the arguments so that we will be able to use the higher-order recursion operator µHO, which is how we will “tie the knot” when defining the believe and Htuple predicates.

–  –  –

cation f : {P }{Q} in Γ, the body of the function f, that is, Ψ(f ), has precondition P and postcondition Q.

The first argument of believe is a function H from Hargs to predicate— that is, a function that has the same type as the Hoare tuple. The higher-order recursion operator µHO will “tie the knot” and make sure that H will be the Hoare tuple itself. The second argument to believe is the predicate Γ, and the third argument is the program Ψ; the purpose of believe is to relate Γ to Ψ using H.

First, believe quantifies over all functions f, preconditions P, and postconditions Q. Then for any function specification f : {P }{Q} that is implied by Γ—that is, if2

–  –  –

which is ! (Γ ⇒ true ∗ f : {P }{Q}).

This implication is very unusual for us in that we almost never use the “unsafe” form of implication ⇒; moreover looking at it now we suspect that unsafe implication is not needed in the proofs. One of many projects for cleaning up the Coq proofs in the future will be to replace ⇒ with ⊂ in the Coq definition of believe.



 We require the ⊲ operator so that believe is contractive in H.

There is a subtlety in this definition involving the quantification over P and Q and the relationship of them to Γ. We are able to quantify over predicates P and Q because we support full impredicative quantifiation. Next, recall from section 7.3.10 that due to the way YES inverts, that for a given function f there are multiple P and Q that will be indistinguishable; all that we know is that they are equivalent at strictly greater approximation. This is another reason for applying the ⊲ operator before we pass P and Q to H.

The Htuple predicate implements our Hoare tuple. We start with the higher-order recursion operator µHO, which was explained in section 7.3.9 and which has type µHO : ∀α. ((α → predicate) → (α → predicate)) → α → predicate.

We instantiate the type parameter α with the type Hargs; then µHO binds the variable H for recursive self reference. Now we provide a function of type Hargs → predicate, which we do with a λ as usual, pattern-matching the arguments (Γ, P, c, Q) of the Hoare tuple.

Now we universally quantify over all programs Ψ, and require

–  –  –

controls κ, if Q guards κ, then P guards c · κ—the difference is that Ψ is no longer a free variable in the definition.

Once our Hoare tuple is defined we can define a notation Γ ⊢ Ψ for believe Htuple Γ Ψ, which is equal to the believe inside the definition of Htuple by fold-unfold.

Finally, we define our “user-level” Hoare tuple Γ ⊢ {P } c {Q} as

–  –  –

using the notation defined in section 7.3.1, where ⊢ P is shorthand for ∀w. w |= P. A Hoare rule is sound only if it is true for all worlds.

–  –  –

We are now ready at last to prove the axioms of CSL sound with respect to the Concurrent C minor oracular semantics. Later, in section 10.3, we will connect the oracular semantics to the concurrent operational semantics and thereby achieve an end-to-end result.

The Hoare rules divide into three categories. The first category, which is by far the most numerous, covers all of the sequential Hoare rules except for call. The second category contains the call rule and the rules for building up the predicate Γ. The third category coveres the concurrent rules.



 10.2.1 Sequential rules In section 2.5.3 we presented the sequential Hoare rules of Appel and Blazy in figure 2.6. Appel and Blazy proved those rules sound in Coq with respect to sequential C minor; their proof was a sizable engineering development, and complex enough without worrying about complexities arising from concurrent computation.

Appel was able to adapt those Coq proofs to our new definitions without altering their essential structure; very little changed, providing strong evidence that our oracular semantics was able to hide the complexities of concurrency from the metatheory proofs about sequential language features, even in the extremely picky context of a machinechecked proof.

10.2.2 Function call The proof of the call rule, on the other hand, did have to change since it interacts with the new Γ ⊢ Ψ predicate. In fact, the semantics of function call had to change so that the resource map was aged during the call; remember from figure 8.1 that rule sstep-call does just that.

Here we prove a simplified CSL call rule where we remove the function arguments, but in the Coq development we prove the rule for the full C minor call statement. We will also assume that P and Q are valid in the sense given in section 7.3.8.

–  –  –

we can then take a step from (w ′, call f · κ) to (w ′′, Ψ(f ) · κ).

By the definition of safety, it suffices to prove this state safe.

We know ⊢ (Γ ∗ f : {P }{Q}) ⊂ (true∗ f : {P }{Q}). Therefore, by the definition of w |= (Γ ∗ f : {P }{Q}) ⊢ Ψ, and since we know that level w ′ ≤ level w, we know that w ′ |= ⊲ Htuple(Γ ∗ f : {P }{Q}, P, Ψ(f ), Q). Since w ′′ is strictly more approximate than w ′ and since Htuple is fashionable, we know that w ′′ |= Htuple(Γ ∗ f : {P }{Q}, P, Ψ(f ), Q).

Γ ⊢ Ψ is fashionable, meaning that it holds on all worlds of the same level. Therefore, from w |= (Γ ∗ f : {P }{Q}) ⊢ Ψ, we know w ′′′ |= (Γ ∗ f : {P }{Q}) ⊢ Ψ for some w ′′′ of the same level as w and such that there exists an n such that

–  –  –

Like all the proofs about sequential features, this proof did not mention anything about concurrency. The ability to prove complicated sequential results that are blind to the fact that they are running in a concurrent context is a major strength of our approach.

Combining proofs about functions The major task for the CSL user is to prove Γ ⊢ Ψ—that is, to prove pre- and postconditions for all of the functions in Ψ. For proving indi

–  –  –

We use the notation Γ ⊢ Ψ : Γ′ as shorthand for believe′ Γ Ψ Γ′.

Γ ⊢ Ψ : Γ′ means that all the functions in Γ′ are proved correct with respect to their function bodies in Ψ. Since a function body may call all functions (not just those proved correct so far), they may use any of the specifications contained in Γ. This allows Γ′ to be built up one function at a time.

To help the user prove Γ ⊢ Ψ, we provide the rules in figure 10.4.

The idea is that we will start with Γ′ as emp, with rule func-nil. Then



 we will add the functions in Γ to Γ′ one at a time, with rule func-cons.

The user will prove each function body using the rules of CSL. When every function in Γ has been added to Γ′, then the two variants of believe are equivalent as expressed in rule func-believe.

Theorem 10.2. The rules func-nil, func-cons, and funcbelieve are sound with respect to the semantic definitions of Γ ⊢ Ψ and Γ ⊢ Ψ : Γ′.

Proof. Rule func-nil is vacuously true since emp does not contain any functions. Rule func-believe is true immediately from the definitions. For rule func-cons, believe′ is quantifying over all of the functions in Γ′ plus the new function f. For all of the functions in Γ′, we use the premise Γ ⊢ Ψ : Γ′. For the new function f, we need to prove ⊢ ⊲ Htuple(Γ, P, Ψ(f ), Q), which follows immediately since for any P, (⊢ P ) → (⊢ ⊲ P ).

–  –  –

The CSL user thus proves the bodies of all his functions with respect to Γ using the rules of CSL, and then uses the rules in figure 10.4 to prove Γ ⊢ Ψ.

10.2.3 Concurrent rules

–  –  –

respect to the oracular semantics.

Theorem 10.3. The rules of Concurrent Separation Logic for the concurrent statements of Concurrent C minor as given in figure 4.1 are sound with respect to the semantics of the Hoare tuple defined in figure 10.3.

Proof. All of the concurrent statements of Concurrent C minor are handled by the consult partial function. Therefore, our job is to show that the preconditions of the rules guarantee that consult does not get stuck and that afterwards the postconditions hold. Since in the definition of safe we universally quantify over all oracles, our proofs must hold

–  –  –

The oracular consult partial function was defined in section

9.3 with three cases. In the first case, Ω-invalid, we handle invalid oracles, where there is no concurrent machine state compatible with the oracle. If the oracle is invalid, we loop endlessly. Since looping endlessly is safe regardless of the precondition, and since a postcondition is possible given an infinite loop, we can easily prove the Hoare rules if we have been given an invalid oracle by the universal quantification.

–  –  –

consistency requirements given in section 8.4. This will be one of our major tasks in the case analysis below.

Assuming that this first task is done and therefore the preconditions are good enough to guarantee that the concurrent step relation is able to step from S to S ′, the consult function cannot get stuck. Therefore, the remaining task in the soundness proof is to prove the postcondition of the CSL rule. The oracle classically decides whether control will ever return to the thread by branching on the StepOthers relation.

In the first case, Ω-diverges, control will never return and the machine enters an infinite loop. As before, this makes it possible to prove any postcondition.

In the final case, Ω-steps, control returns after running the other threads. In this case it is necessary to use the precondition of the CSL rules to prove their postcondition by doing induction on the StepOthers relation.

–  –  –

An examination of the make lock case of the consult function defined in figure 8.2 will make clear that the consult will not get stuck and will guarantee the postcondtion. The concurrent machine will run cstep-seq to execute this instruction. Since the new lock is created locked, it is simple to show that the machine is still consistent since we only require complex properties to

–  –  –

An examination of the free lock case of the consult function defined in figure 8.2 will make clear that the consult will not get stuck and will guarantee the postcondtion. The concurrent machine will run cstep-seq to execute this instruction. Since we have removed a lock from the total resouce map φT, it is easy to show consistency of the new state because we can quantify over one fewer lock.

–  –  –

the consistency requirements on lock pools it is simple to show a postcondition of ⊲ tightly R, but this is not good enough to prove our CSL rule, since we need tightly R, which is stronger. Accordingly, we need to make a more complex induction, where we argue that since the time when the lock was unlocked, we have already context switched at least once, and therefore we have moved from ⊲ tightly R to tightly R.

–  –  –

An examination of the preconditions of the CSL rule will demonstrate that the concurrent machine will run cstep-unlock to execute this instruction. Proving the postcondition of emp is not difficult. The difficulty is in showing that the new machine state is consistent, and in particular that the rules for the lock pool are

–  –  –

5. Γ ⊢ {f : {P }{Q}∗validly precisely P } forkf {f : {P }{Q}} An examination of the preconditions of the CSL rule will demonstrate that the concurrent machine will run cstep-fork to execute this instruction. It is not difficult

–  –  –

oracle semantics to the concurrent semantics in section 10.3, we will have to prove that the has been properly started in the preservation theorem.

–  –  –

Pages:     | 1 |   ...   | 17 | 18 || 20 | 21 |   ...   | 22 |

Similar works:

«A MOLECULAR INVESTIGATION OF ADSORPTION ONTO MINERAL PIGMENTS BY Brian J. Ninness B.S. University of Pittsburgh, 1995 M.S. University of Maine, 1997 A THESIS Submitted in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy (in Chemical Engineering) The Graduate School The University of Maine December, 200 1 Advisory Committee: Carl Tripp, Associate Professor of Chemistry and LASST, Co-Advisor Douglas Bousfield, Professor of Chemical Engineering, Co-Advisor Bill...»

«AN Abstract OF THE DISSERTATION OF Shon Schooler for the degree of Doctor of Philosophy in Entomology presented on December 1, 2003. Title: Negative Effect of Purple Loosestrife and Reed Canary Grass on the Diversity of Wetland Plant and Moth Communities. Abstract approved: _ Peter B. McEvoy Invasive plants have the potential to reduce the diversity of species in plant and animal communities. I examined the negative effect of two invasive wetland plants, purple loosestrife and reed canary...»

«Sky Woman's Great Granddaughters: A Narrative Inquiry Into Kanienkehaka Women's Identity Kahente Horn-Miller A Thesis in The Humanities Program Presented in Partial Fulfillment of the Requirements For the Degree of Doctor of Philosophy at Concordia University Montreal, Quebec, Canada September 2009 © Kahente Horn-Miller, 2009 1*1 Bibliotheque et Library and Archives Archives Canada Canada Direction du Published Heritage Branch Patrimoine de I'edition 395 Wellington Street 395, rue Wellington...»

«Redefining car-bus interchange to reduce traffic by Stuart Daniel Meek A Doctoral Thesis Submitted in partial fulfilment of the requirements for the award of Doctor of Philosophy of Loughborough University June 2010 © by Stuart Meek 2010 Thesis Access Form Copy No..Location.. Author Stuart Daniel Meek Title Redefining car-bus interchange to reduce traffic Status of access Open Moratorium Period:.years, ending./.200. Conditions of access approved by (CAPITALS):.. Supervisor (Signature)......»

«Physics College of Science Graduate Programs 2014-1015 Contents Faculty 1 The Graduate Programs 5 The Doctor of Philosophy Degree 6 The Master of Science Degree 15 Our Mission: To educate students for a life of fulfillment and accomplishment. To Create and translate knowledge to meet global and societal needs. Northeastern University is an equal opportunity/affirmative action Title IX education institution and employer. Tuition rates, all fees, rules and regulations, courses, and course content...»

«La libertà nella filosofia di L P. Sartre Gli esistenzialisti si sono presentati alla massa facilmente riconoscibili per il loro aspetto, disobbedienti ad ogni vincolo di moda, di costumi e di educazione, nella varietà di uomini e donne provenienti dai più diversi strati della società. Così, sulla scorta dei resoconti e delle curiosità giornalistiche, la massa si è abituata a vedere l'Esistenzialismo come movimento bizzarro, e più ancora, come atteggiamento di una casta di artisti...»


«The Concept of Self-Reflexive Intertextuality in the Works of Umberto Eco by Annarita Primier A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Centre for Comparative Literature University of Toronto © Copyright by Annarita Primier 2013 ii The Concept of Self-Reflexive Intertextuality in the Works of Umberto Eco Annarita Primier Doctor of Philosophy Centre for Comparative Literature University of Toronto 2013 Abstract Umberto Eco’s novels are...»

«TOWARDS A COGNITIVE THEORY OF THE FIRM Issues and a logic of change 1 third version, june 1996 Bart Nooteboom2 e-mail b.nooteboom@bdk.rug.nl SOM theme B: Inter-firm Coordination and Change: Marketing and Networks Abstract The paper consists of three parts. The first part gives an inventory of issues that no cognitive theory of the firm can ignore. These are grouped into three themes: aspects of development, issues of coordination and philosophy of knowledge and language. The second part of the...»

«CHARACTERISTICS OF WEB-BASED TEXTUAL COMMUNICATIONS A DISSERTATION SUBMITTED TO THE DEPARTMENT OF COMPUTER ENGINEERING GRADUATE SCHOOL OF ENGINEERING AND SCIENCE AND THE OF BILKENT UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY By u¸ ¨ Tayfun K¨ cukyılmaz December, 2012 I certify that I have read this thesis and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of doctor of philosophy. Prof. Dr....»

«THE INTEGRATION OF LANGUAGE AND CONTENT: FORM-FOCUSED INSTRUCTION IN A CONTENT-BASED LANGUAGE PROGRAM by Antonella Valeo A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Graduate Department of Curriculum Teaching and Learning Ontario Institute for Studies in Education University of Toronto © Copyright by Antonella Valeo (2010) THE INTEGRATION OF LANGUAGE AND CONTENT: FORM-FOCUSED INSTRUCTION IN A CONTENT-BASED LANGUAGE PROGRAM Doctor of Philosophy,...»

«MANAGING VARIABILITY IN VLSI CIRCUITS by Brian T. Cline A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Electrical Engineering) in The University of Michigan Doctoral Committee: Professor David Blaauw, Chair Professor Marios Papaefthymiou Associate Professor Joanna Mirecki-Millunchick Associate Professor Dennis M. Sylvester © Brian T. Cline All Rights Reserved DEDICATION To my Family & Friends. This dissertation is dedicated to my...»

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