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



Pages:     | 1 |   ...   | 16 | 17 || 19 | 20 |   ...   | 22 |

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

-- [ Page 18 ] --

The final case, rule Ω-steps, is when control returns after running the other threads. In this case we project out the ith thread from the new concurrent machine state S ′′ and proceed with the new oracle, world, and control that came from running the concurrent machine.

–  –  –

rent machine itself requires classical reasoning to find a world satisfying an unlock assertion because we allow users to use a classical logic, and second, determining whether control will return to a given thread reduces the halting problem. The nonconstructivity of our operational semantics is not a bug: we are not building an interpreter, we are building a specification for correctness proofs of compilers and program logics.

–  –  –

As explained in section 6.6, we define the oraclular step relation using the consult relation. As explained in that section, the oracular step uses the underlying step relation (which is the step relation for sequential C minor) when executing core statements.

We use the oracular step to keep “unimportant” details of the concurrent machine from interfering with proofs about the sequential language. The key features of the oracular step are the following:

1. It is deterministic, which simplifies sequential metatheory

2. When it encounters a synchonization operation, it is able to make progress with the oracle, whereas a regular step relation gets stuck

3. It composes with itself, whereas the regular step relation does not (because memory will change between steps due to other threads)

–  –  –

With these properties we can prove properties of the sequential features of Concurrent C minor in a natural way.

9.5 Conclusion In chapter 8 we gave Concurrent C minor a formal concurrent operational semantics. That semantics was easy to use for reasoning about the concurrent features of the language, but not natural to use for reasoning about sequential features. In this chapter we have defined an oracular semantics for Concurrent C minor to support natural reasoning about sequential features.

We have not yet formally stated the precise relationship between the oracular semantics and the concurrent semantics. The oracular semantics is built from the concurrent semantics, but we wish to reason somewhat differently. The oracular semantics is a “thread-local” version of the semantics, so it is natural to think that if we could prove properties of each thread using the oracular semantics, then we could combine those proofs into a proof of the entire concurrent machine.

However, we are not yet in a position to formally state the connection, which will be the subject of section 10.3.

Chapter 10 A Modal Hoare Judgment and Oracular Soundness In chapter 3 we introduced Concurrent C minor. In chapter 4 we gave Concurrent C minor an axiomatic semantics, Concurrent Separation Logic. In chapter 8 we gave Concurrent C minor an operational semantics. At last we are ready to connect these two semantics by proving the soundness of the CSL axioms with respect to the operational semantics.

Our CSL axiomatic semantics is designed to reason about one thread at a time, and we noted in chapter 8 that the concurrent operational semantics was not particularly easy to use for reasoning about such sequential computation. In chapter 9 we developed an oracle semantics that presents a single-threaded view of the concurrent machine and is suitable for reasoning about one thread at a time.

We connect our axiomatic semantics to our operational semantics in

–  –  –

Here we develop the definition for the Hoare tuple. First, in section 10.1.1, we explain a simple continuation-passing definition in the style of Appel and Blazy [AB07]. Then in section 10.1.2 we explain why this style of definition will not allow us to embed predicates into program syntax as we wish to do for the make lock statement of Concurrent C minor. Finally, we show how to redefine the Hoare tuple using our modal logic of chapter 7 and explain how the new definition allows us to embed predicates into program syntax.

10.1.1 A continuation-passing Hoare judgment Our semantic model for Hoare tuples is rooted in the idea of safety, defined in figure 10.1. We start with the notion of immediately safe.

A state σ is immediately safe if it is not stuck; in other words, if it is safely halted or can take a step. A state can be safely halted in two Portions of this chapter have been published before as [HAZ08a] and [HAZ08b].

10.1. A MODAL HOARE JUDGMENT 

–  –  –

ways. The first, case isafe stop, is the standard way of saying that the machine has been safely halted when the code has reached the end of the computation. The second, case isafe level, is less standard. After we reach approximation level 0, we will no longer be able to age the resource maps; moreover, all of the stratified predicates are now unit and therefore no longer guarantee anything.

This does not mean that the program is now unsafe; it means that the program’s observer has stopped caring about the computation. We prove our programs sound starting with arbitrarily large amounts of stratification. Therefore, our programs are proved sound with regard to any finite amount of time. If we wish to know that our program is safe

CHAPTER 10. A MODAL HOARE JUDGMENT AND





ORACULAR SOUNDNESS

 for 100 steps of computation, we stratify predicates to level 100 (we age the world at most once per step of computation). If we wish to know that our program is safe for 100 billion steps of computation, we stratify predicates to level 100 billion. The third way of being immediately safe, case isafe step, is the standard way of observing that if we can take a step then we are not stuck.

We define the −→∗ relation in the usual way as the composition of the −→ relation with cases stepstar 0 and stepstar S. We then dene safe in the usual way: for any state σ ′ reachable from σ, σ ′ is immediately safe. Notice that we quantify universally over all initial oracles Ω; in section 9.3 we explained that quantifying over all oracles instead of simply valid ones is sound due to the Ω-invalid case of the oracular consult relation: if we get an invalid oracle we are safe if we try to consult it because we loop forever. The unrestricted universal quantification simplifies the proofs that do not use the oracle since it means that they do not have to carry around validity premises about the oracle, which would weaken the isolation between the sequential and concurrent reasoning.

–  –  –

Blazy. This is a simpler definition than the one they use, which supports the frame rule in a more semantic style, and has additional parameters to handle nonlocal exits from blocks and functions. Their rule was given

10.1. A MODAL HOARE JUDGMENT 

–  –  –

Figure 10.2: Na¨ continuation-passing style definition of Hoare tuple ıve in full in figure 2.

5 in chapter 2. In the Coq development we include all of the features they describe to handle the nonlocal exits and semantic frame rule, but here we eliminate many of the more advanced features, which are for sequential control flow, to concentrate on the key ideas.

–  –  –

Next, we define the Hoare tuple Γ ⊢ {P } c {Q}. For any sequence of instructions κ, if Γ ∗ Q guards κ then Γ ∗ P must guard the statement c followed by κ. We add the parameter Γ, which is the assertion that describes the functions, to both the pre- and postconditions as a convenience for the user, so that he does not have to write {Γ ∗ P } c {Γ ∗ Q}.

This is a continuation-passing style definition, and it may not be obvious at first glance that it is equivalent to the informal notion of “if we start with a state that satisfies P, and we run s, and s terminates,

CHAPTER 10. A MODAL HOARE JUDGMENT AND

ORACULAR SOUNDNESS

 then we end with a state that satisfies Q”. It is equivalent because we are quantifying over all instruction sequences κ that are guarded by Q.

For any property of Q that is checkable with our operational semantics, we can develop a small tester sequence that tests the property and gets stuck if it does not hold. If we are still concerned, it is easy to add a statement that asserts that the predicate Q holds and if it does not then gets stuck.

This definition is one of partial correctness; in other words it does not assume that the statement s will terminate. However, since it asserts that s · κ is safe if P holds, then it does imply that the statement s does not get stuck.

Using this definition, we can prove all of the sequential rules of separation logic except for the rule for call. In fact, as mentioned above, Appel and Blazy use a more complex version of this definition to prove all of the rules of sequential separation logic with respect to C minor in Coq. Unfortunately, in the current context, we cannot use the definition of the Hoare tuple given in figure 10.2 to prove the soundness

of the function call CSL rule:

–  –  –

The problem is that the program Ψ, used in function call to match a function name with a function body, is free in the definition of the Hoare rule. Obviously, a sound definition should not have any free variable;

10.1. A MODAL HOARE JUDGMENT  unfortunately, fixing the problem is not easy. One solution is to make Ψ a parameter of the Hoare tuple, an approach taken by Schirmer [Sch06]. However, this solution requires the CSL use to drag around his entire program through his correctness proofs, which is unfortunate, and makes function pointers more difficult to use. Moreover, the user already is passing around a description of the functions in Γ—why should he also pass around the program Ψ?

We cannot simply quantify universally over the program Ψ; this makes the call rule easy to use—but impossible to prove, so it will not do. Another bad idea is to quantify existentially over the program Ψ;

this makes the call rule easy to prove—but impossible to use.

We are fast running out of options. Appel and Blazy put the program Ψ into the world w and let predicates judge program syntax.

However, in our context this solution is not good enough since we do not wish to put program syntax into worlds.

10.1.2 Embedding predicates into syntax We cannot put program syntax into the world due to the make lock l R statement. This statement takes a semantic predicate R—i.e., a function from world to Prop—that becomes the resource invariant of the new lock l. Thus, a predicate is embedded into program syntax.

Since program syntax is directly exposed to the user, we wish to provide a simple inductive definition for program syntax and avoid complex stratification techniques. If we wish to avoid stratification techniques,

CHAPTER 10. A MODAL HOARE JUDGMENT AND

ORACULAR SOUNDNESS

 then the definition for the type of “predicate” must come before the definition of program syntax. Since a predicate is a function from world to Prop, a world cannot contain program syntax, which is why a world is simply a tuple of locals ρ, resource map φ, and memory m.

One very important predicate is f : {P }{Q}, i.e., “f is a function

–  –  –

definition of the Hoare tuple, there was no relation at all, since Ψ was a free variable.

As we discussed, we do not wish to provide Ψ as a parameter to the Hoare tuple. Instead, what we want to do is quantify over all “good” programs Ψ – that is programs compatible with Γ. The idea is to add an additional premise after a universal quantification; this way we hope to have a definition that is both possible to use and possible to prove.

What we are looking for is some relation Γ ⊢ Ψ, called the believe relation, which says that the program Ψ is compatible with Γ. Compatible with Γ means that if there is an assertion f : {P }{Q} in Γ, then we can believe that assertion about the function body Ψ(f ).

–  –  –

Recall that we use ≈ to mean “we wish we could define things this way”. This definition says that for any program Ψ compatible with Γ, if Q guards κ, then P must guard c · κ.

What remains is to define the relation Γ ⊢ Ψ. The obvious choice is

–  –  –

In other words, for any function assertion that is part of Γ, the Hoare tuple guarantees that the body of that function has precondition P and postcondition Q.

Unfortunately, there is a problem with these definitions: the definition of the Hoare tuple depends on the believe relation, while the definition of the believe relation depends on the definition of the Hoare tuple. Worst of all, this dependence is contravariant, meaning that no solution exists, even in untyped set theory.

–  –  –

Fortunately, we have our modal logic from chapter 7, which was developed to handle just this kind of thorny contravariant recursive situation.

CHAPTER 10. A MODAL HOARE JUDGMENT AND

ORACULAR SOUNDNESS

 Although we originally developed it to model lock invariants, we can use it to define the Hoare tuple itself since the logic has powerful features such as impredicative quantification and higher-order recursion.

The Hoare tuple we explain here is much simpler than the one in

the Coq development. The major simplifications include:

1. No globals in the world type. As in chapter 7, we removed from the world type the map from global names to addresses.

2. No relation between function pre- and postconditions. As in chapter 7, we have removed the extra parameter that relates function pre- and postconditions to each other.

3. No marshaling of arguments. As explained in chapter 8, we have a method of marshaling arguments at function call so that our function preconditions can judge them. We omit this feature here for simplicity.



Pages:     | 1 |   ...   | 16 | 17 || 19 | 20 |   ...   | 22 |


Similar works:

«COMMENCEMENT EXERCISES University of Notre Dame Notre Dame, Indiana Graduate School College of Arts and Letters College of Science College of Engineering College of Law College of Commerce In the University Gymnasium At 8:00 p. 1n. (Central War Tim.c) December 20, 1942 Program Grand Processional March, by the University Orchestra The Conferring of Degrees, by Rev. J. Hugh O'Donnell, c.s.c., President of the University Commencement Address, by the Honorable William Martin Jeffers, Rubber...»

«MODULATION OF AUTOIMMUNE DIABETES BY B LYMPHOCYTES SPECIFIC FOR N-ACETYL-D-GLUCOSAMINE by BRIAN LEONARD PUNZALAN DIZON JOHN F. KEARNEY, CHAIR DAVID D. CHAPLIN LOUIS B. JUSTEMENT MOON NAHM HUBERT M. TSE A DISSERTATION Submitted to the graduate faculty of The University of Alabama at Birmingham, in partial fulfillment of the requirements for the degree of Doctor of Philosophy BIRMINGHAM, ALABAMA i MODULATION OF AUTOIMMUNE DIABETES BY B CELLS SPECIFIC FOR NACETYL-D-GLUCOSAMINE BRIAN L. P. DIZON...»

«THREE-DIMENSIONAL FINITE-ELEMENT TIME-DOMAIN MODELING OF THE MARINE CONTROLLED-SOURCE ELECTROMAGNETIC METHOD A DISSERTATION SUBMITTED TO THE DEPARTMENT OF GEOPHYSICS AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Evan Schankee Um March 2011 Abstract The marine controlled-source electromagnetic (CSEM) method detects and images electrical resistivity associated with hydrocarbon, gas and CO2 reservoirs....»

«OFF THE FIELD: AN EMPIRICAL EXAMINATION OF THE IMPACT OF ATHLETE TRANSGRESSIONS AND RESPONSE STRATEGY ON THE IMAGE REPAIR AND CRISIS COMMUNICATION PROCESS by KENON ASHANTI BROWN BRUCE K. BERGER, COMMITTEE CO-CHAIR EYUN-JUNG KI, COMMITTEE CO-CHAIR J. SUZANNE HORSLEY ANDREW C. BILLINGS ARTHUR W.ALLAWAY A DISSERTATION Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in the College of Communication and Information Sciences in the Graduate School of The...»

«University of Alberta Gertrude Stein’s Cubist Brain Maps by Lorelee Kim Kippen A thesis submitted to the Faculty of Graduate Studies and Research in partial fulfillment of the requirements for the degree of Doctor of Philosophy Department of Comparative Literature ©Lorelee Kim Kippen Fall 2009 Edmonton, Alberta Permission is hereby granted to the University of Alberta Libraries to reproduce single copies of this thesis and to lend or sell such copies for private, scholarly or scientific...»

«ASKING THE QUESTION: ‘WHAT IS ORGANIZATION?’ Thesis submitted for the degree o f Doctor o f Philosophy at the University o f Leicester by Sverre Spoelstra School of Management University of Leicester December 2006 UMI Number: U219244 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 manuscript and there are missing pages, these will be noted. Also,...»

«THE UNIVERSITY OF CHICAGO YEARNING FOR A DREAMED REAL: THE PROCESSION OF THE LORD IN THE TAMIL ULĀS A DISSERTATION SUBMITTED TO THE FACULTY OF THE DIVINITY SCHOOL IN CANDIDACY FOR THE DEGREE OF DOCTOR OF PHILOSOPHY BY BLAKE TUCKER WENTWORTH CHICAGO, ILLINOIS DECEMBER 2011 For my beloved parents, Carl M. Wentworth and Carolyn S. Wentworth அ ா ா ா கால யா ர ைட ா ள டல க ல ல க ா வ டல ப ல கற ப ா வா ைல ா டல ர க ா ா...»

«THE EFFECTS OF ELEMENTARY DEPARTMENTALIZATION ON MATHEMATICS PROFICIENCY Nicole C. Taylor-Buckner Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy under the Executive Committee of the Graduate School of Arts and Sciences COLUMBIA UNIVERSITY © 2014 Nicole C. Taylor-Buckner All rights reserved ABSTRACT THE EFFECTS OF ELEMENTARY DEPARTMENTALIZATION ON MATHEMATICS PROFICIENCY Nicole C. Taylor-Buckner Mathematics education in the elementary schools has...»

«MICRO ELECTRET POWER GENERATORS Thesis by Justin Boland In Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy CALIFORNIA INSTITUTE OF TECHNOLOGY Pasadena, California (Defended May 24, 2005) ii © 2005 Justin Boland All Rights Reserved iii ACKNOWLEDGEMENTS Yu-Chong Tai, Trevor Roper, Tanya Owen, Wen Hsieh, Ellis Meng, Tom Tsao, Mattieu Liger, Qing He, Chi-Yuan (Victor) Shih, Scott Miserendino, Po-Jui (PJ) Chen, Nick Lo, Jayson Messenger, Svanhild (Swan) Simonson,...»

«The Techneducator Effect: Colliding Technology and Education in the Conceptualization of Virtual Learning Environments Daniel Jason Nolan A thesis subrnitted in conforrnity with the requirements for the degree of Doctor of Philosophy Department of Curriculum, Teaching and Learning Ontario Institute for Studies in Education of the University of Toronto O Copyright by Daniel Jason Nolan (2001) Bibliothèque nationale 1*1 National Library du Canada o Canada f Acquisitions and Acquisitions et...»

«Three-dimensional nanofabrication of silver structures in polymer with direct laser writing A dissertation presented by Kevin Lalitchandra Vora to The School of Engineering and Applied Sciences in partial fulfillment of the requirements for the degree of Doctor of Philosophy in the subject of Applied Physics Harvard University Cambridge, Massachusetts February 2014 ©2014 Kevin Lalitchandra Vora All rights reserved. Dissertation advisor: Professor Eric Mazur Kevin Lalitchandra Vora...»

«© Copyright, Princeton University Press. No part of this book may be distributed, posted, or reproduced in any form by digital or mechanical means without prior written permission of the publisher. I Nihilism Curiosity about the world, as we know, sometimes leads to philosophy. It can happen when that curiosity cannot be satisfied by knowledge of one or another event, by knowledge of one or another contingency, or by discovering the causes behind one or another phenomenon. It happens when we...»





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