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



Pages:     | 1 |   ...   | 18 | 19 || 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 20 ] --

Now that we have proved all of the rules of CSL sound with respect to the oracular semantics of Concurrent C minor, half of our soundness task is done. The other half, covered in the remainder of this chapter, is to connect the oracular semantics to the concurrent semantics, which we do with progress and preservation theorems.

CHAPTER 10. A MODAL HOARE JUDGMENT AND

ORACULAR SOUNDNESS



–  –  –

Now we connect the oracular semantics to the concurrent semantics.

First we define the notion of concurrent safety in figure 10.5. We say that a concurrent machine state S is concurrently immediately safe (just referred to as immediately safe when the context is clear) in three situations.

First, case c isafe level, the concurrent machine is immediately safe if the resource maps inside it have approximation level 0. Recall that since all resource maps in S must join together due to the consistency

10.3. SOUNDNESS OF THE ORACULAR APPROACH  requirements on S, all those resource maps must have the same approximation level, and therefore it is sufficient to test the level of the alloc pool. Just as in section 10.1.1, we only provide guarantees about correct behavior for an arbitrarily large but finite amount of time.

Second, case c isafe sched, the concurrent machine is immediately safe if the schedule is trying to pick a nonexistent thread. Since we quantify over all schedules we do not have to worry that some of the schedules we quantify over wish to pick nonexistent threads; we also quantify over all schedules that pick only existing threads.

Third, case c isafe step, the concurrent machine is immediately safe if it can take a step. That is, “immediately safe” means “not stuck”.

We define the =⇒∗ relation as the composition of the concurrent step relation in the usual way with cases cstepstar 0 and cstepstar S.

We define csafe in the usual way: for any state S ′ reachable from S, S ′ is immediately safe.

Our major goal will be to prove concurrent safety from oracular safety. Due to the nature of the concurrent step relation, concurrent safety is actually quite a strong property. Recall from section 8.5 that the cstep-unlock rule requires that a lock’s resource invariant be true before unlocking. This means that concurrent safety implies that all resource invariants are obeyed. Since outside programs can only communicate with a program via locks, this implies that all outside communication is done correctly.

–  –  –

vation theorem. As usual, the progress theorem will define an invariant sufficient to guarantee that the concurrent machine is not stuck and the preservation theorem will guarantee that the invariant is preserved as the machine computes.

–  –  –

In figure 10.6 we define the property safe-as i. Informally, a concurrent continuation (Ω, σ, κ) is safe-as i if, supposing it is the ith thread of the ˆ concurrent machine consistent with oracle Ω, then if this thread is ever ready to run then it will be oracularly safe. There are two cases: in the first, case safe-as never, the thread will never again be selected to run sequential code again; in the second, case safe-as eventually, the thread

10.3. SOUNDNESS OF THE ORACULAR APPROACH  will eventually be selected to run again, and when it is selected, it will be safe. Recall that to be safe we must quantify over all oracles, so we do not need to worry about the actual oracle Ω′.

We define Ψ ⊢ all-threads-safe(S) to mean that each projection of S will be oracularly safe the next time it is ready and selected. Together with the consistency requirements on the concurrent machine state as explained in section 8.4, this is enough to prove progress.

Theorem 10.4 (Progress). If Ψ ⊢ all-threads-safe(S), then S is immediately safe.

Proof. Part of taking a step in the concurrent machine is proving that the next concurrent machine has the consistency property. More than half of the difficulty in the theorem is proving consistency of the next concurrent machine state. These properties would normally be proved in the preservation theorem, but due to the use of dependent types to guarantee consistency part of the preservation theorem is proved in the progress theorem.

By case analysis on the thread whose thread-id is at the head of the schedule. The initial case is on the concurrent control of the thread.

–  –  –

2. The concurrent control is Krun κ, so the thread is runnable.

We have two cases. Since thread i is at the head of the schedule, we know Ψ ⊢ StepOthers i S S. By allthreads-safe we know safe-as i, where i is the thread at the head of the schedule; there are two possibilities, but we know that it cannot be safe-as never, since thread i is ready to run. Therefore it must be safe-as eventually, and thread i must be oracularly safe. If it is safe because the thread has reached Kstop then we execute cstep-texit. Otherwise, the thread must be able to take

an oracular step. There are three possibilities:

–  –  –

10.3.2 Preservation The preservation theorem is more complex due to the existence of forks, since we need to know that the child will be safe if its precondition is satisfied. To guarantee that the child will be safe, we require an additional invariant, all-funs-spawnable, given in figure 10.7.





CHAPTER 10. A MODAL HOARE JUDGMENT AND

ORACULAR SOUNDNESS

 First we define the predicate version of the rkind function, prkind, which maps resources to resource kinds. Recall from section 8.4.6 that rkind is useful as an antecedent with unrestricted (dangerous) implication, and we will use prkind here for this purpose. If

–  –  –

then φ @ l has resource kind k.

Then we define Ψ ⊢ all-funs-spawnable(S). Recall that for any concurrent machine state S there exists a total resource map φT that is the join of all of the resource maps in S. all-funs-spawnable states that there exists a predicate Γ that is compatible with the program Ψ and that for any location f with kind kFUN, there exists a precondition P and postcondition Q such that

–  –  –

and that Γ implies, i.e. all the functions in φT are contained in Γ.

Together this means that all of the functions in Ψ are conservatively approximated by their pre- and postconditions in Γ. We use the prkind construction and quantify existentially instead of universally over the precondition P and postcondition Q here for the same reason as in

–  –  –

The predicate Γ is constructed by the user using the rules of CSL as explained in section 10.2.2.

Lemma 10.1.

If Ψ ⊢ all-funs-spawnable(S), and Ψ ⊢ S =⇒ S ′, then Ψ ⊢ all-funs-spawnable(S ′ ).

Proof. Proved by case analysis on the step relation.

In all cases except for cstep-seq, the total resource map φT does not change except perhaps becoming more approximate (resources are transfered from one part of the machine to another, but this does not change the total resource map).

In step cstep-seq, the total resource map does not get larger or add new functions. The use of rkind ensures that our use of “dangerous” implication is sound even as the total resource map becomes more approximate in much the same

–  –  –

Lemma 10.2.

If Ψ ⊢ all-threads-safe(S), Ψ ⊢ all-funs-spawnable(S), and Ψ ⊢ S =⇒ S ′, then Ψ ⊢ all-threads-safe(S ′ ).

Proof. There are three basic cases. The first is that we need to show that the thread that was just selected and run is As of the writing of this thesis, the Coq proof of the preservation theorem is currently broken due to maintenence and cleaning elsewhere in the system, particularlly related to the function pool φfp ; however everything here claimed to be proved in Coq has been proved in Coq at one time.

CHAPTER 10. A MODAL HOARE JUDGMENT AND

ORACULAR SOUNDNESS

 still safe. The second is that we need need to show that one of the threads that was not selected is still safe. The third only occurs with the fork rule, and it is when we need to show that the new child thread is safe.

–  –  –

Theorem 10.5 (Preservation). If Ψ ⊢ all-threads-safe(S), Ψ ⊢ all-funs-spawnable(S), and Ψ ⊢ S =⇒ S ′, then Ψ ⊢ all-threads-safe(S ′ ) and Ψ ⊢ all-funs-spawnable(S ′ ).

Proof. By lemmas 10.1 and 10.2.

–  –  –

10.3.3 Safety Now that we have both the progress and preservation theorems, we are ready to prove concurrent safety from oracular safety.

Theorem 10.6 (Safety). If Ψ ⊢ all-threads-safe(S) and Ψ ⊢ all-funs-spawnable(S), then Ψ ⊢ csafe S.

Proof. By induction on the =⇒∗ relation and the progress and preservation theorems.

–  –  –

We are nearly done. Recall that a program in Concurrent C minor begins with a call to a special main function.

Corollary 10.1. For any schedule ℧ and arbitrary stratifi

–  –  –

By the definition of the Hoare tuple we can prove the initial call to the main function safe on any world that satisfies its precondition.

Therefore we have the following theorem, expressed as a deductive rule:

–  –  –

then the unerased concurrent machine state (℧, θ :: nil, L0, φmp, φfp, m) is safe.

Proof. Proved from corollary 10.1.

How hard will this theorem be for the CSL user to use? Premise 1 is developed by the user using the rules of CSL as explained in section 10.2.2. Premise 2 is simple: a function pool of arbitrary stratification can be built from Γ by the user. Premise 3 is simple: an alloc pool of arbitrary stratification can be built. Premise 4 is simple: the empty lock pool is easy to construct. Premise 5 is simple as long as the user does not forget the main function. Premise 6 is simple; the single thread is easy to construct. The difficulty of premise 7 depends entirely on how difficult the user wishes to make the precondition of main to satisfy; we point out that emp is very easy to satisfy.

Therefore, we have shown that if a user proves his program sound with CSL, then assuming that his main function’s precondition is satisable his program will be safe when run on the concurrent machine. Our only remaing task is to connect to the erased concurrent operational semantics from chapter 5.

–  –  –

Note: No parallel decomposition lemma. Unlike in previous work [Bro07], we do not require a parallel decomposition lemma. We can avoid such a lemma because

1. We put resource maps into the concurrent operational semantics.

2. In the progress lemma we prove that the next state obeys the consistency requirements, which guarantees that the threads have disjoint resource maps.

3. In the store operation in the sequential semantics we get stuck if we try to write to memory we do not own.

4. We prove the safety of the parent in the CSL fork rule.

5. We prove the safety of the child in the preservation lemma.

In previous semantics the parallel decomposition lemma was a source

–  –  –

In chapter 3 we introduced Concurrent C minor. In chapter 4 we gave Concurrent C minor an axiomatic semantics, Concurrent Separation Logic, and in chapter 8 we gave Concurrent C minor an operational semantics. We have now proved our logic sound with respect to our operational semantics.

Chapter 11

Conclusions and FutureWork

We have proved the soundness of a sophisticated Concurrent Separation Logic with first-class locks and threads with respect to the concurrent operational semantics of Concurrent C minor. Our soundness proof is largely implemented in Coq in a highly modular way, so that the actions of other threads do not complicate the parts of the soundness proof about sequential features and the complexities of sequential control flow do not complicate the parts of the proof about the concurrent features. Moreover, we have a strategy for applying our techniques to the CompCert certified compiler, so that in the future we will be able to have an end-to-end result: proved properties of concurrent source programs will be true of the code that executes on the machine.

In chapter 3 we presented the Concurrent C minor language and

–  –  –

gave an example program in section 3.2. Then in chapter 4 we developed a new concurrent separation logic and demonstrated its power by using it to verify an example program. In chapter 5 we gave Concurrent C minor a formal erased concurrent operational semantics.

In chapter 6 we presented engineering techniques that allow for significant modularization, particularly in the context of a compiler with multiple intermediate languages.

In chapter 7 we developed a new modal substructural logic and showed how to reason about complex parts of the underlying model by reasoning in the logic.

In chapter 8 we developed an unerased concurrent operational semantics that was easier to reason about than the erased concurrent operational semantics from chapter 5. We proved an erasure theorem that showed that the unerased semantics was a conservative approximation to the erased semantics.

The concurrent operational semantics of chapter 8 was not easy to use for reasoning about the sequential features of the Concurrent C minor language, so in chapter 9 we developed a thread-local oracle semantics for it.

Finally, in chapter 10 we developed a new modal Hoare tuple using the oracle semantics and showed how to use it to prove the rules of CSL sound. We also showed how to combine results from the oracular semantics into a result on the concurrent semantics with a progress and preservation lemma, thereby proving the soundness of Concurrent



Pages:     | 1 |   ...   | 18 | 19 || 21 | 22 |


Similar works:

«JOB STRESS, JOB SATISFACTION AND INTENTION TO LEAVE AMONG NEW NURSES by Jessica Zara Peterson A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Graduate Department of Nursing Science University of Toronto © Copyright by Jessica Zara Peterson 2009 ABSTRACT Job Stress, Job Satisfaction and Intention to Leave Among New Nurses Jessica Zara Peterson Doctor of Philosophy Graduate Department of Nursing Science University of Toronto The difficulties new...»

«Optical Spectroscopy and Magnetic Field Profile Measurements on the Self Magnetic Pinch Diode by Sonal Patel 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 2016 Doctoral Committee: Professor Ronald M. Gilgenbach, Chair Mark D. Johnston, Sandia National Labs Professor Yue Y. Lau Assistant Professor Louise Willingale DEDICATION To family and friends. ii...»

«DEVITRIFICATION OF IRON BASED METALLIC GLASSES AT HIGH PRESSURES AND HIGH TEMPERATURES by ANDREW KEVIN STEMSHORN VOHRA, YOGESH K. (CHAIR) CATLEDGE, AARON S HARRISON, JOSEPH G. JANOWSKI, GREGG STOLZ, GUNTER KHARLAMPIEVA, EUGENIA A DISSERTATION Submitted to the graduate facility of The University of Alabama at Birmingham in partial fulfillment of the requirements for the degree of Doctor of Philosophy BIRMINGHAM, ALABAMA 2013 Copyright by ANDREW KEVIN STEMSHORN 2013 DEVITRIFICATION OF IRON BASED...»

«ARCHIVING AUTHORS: RETHINKING THE ANALYSIS AND REPRESENTATION OF PERSONAL ARCHIVES by Jennifer Lynn Douglas A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Faculty of Information University of Toronto © Copyright by Jennifer Douglas 2013 Archiving Authors: Rethinking the Analysis and Representation of Personal Archives Jennifer Lynn Douglas Doctor of Philosophy Faculty of Information, University of Toronto Abstract Personal archives are those...»

«The Jews of the Desert: Colonialism, Zionism, and the Jews of the Algerian M’zab, 1882-1962 by Rebecca A. Wall A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (History) in the University of Michigan 2014 Doctoral Committee: Associate Professor Joshua H. Cole, Co-Chair Emeritus Professor Todd M. Endelman, Co-Chair Associate Professor Carol B. Bardenstein Associate Professor Rita C-K Chin © Rebecca A. Wall 2014 Acknowledgements This...»

«Everyday Enchantments and Secular Magic in Montréal By Ian Alexander Cuthbertson A thesis submitted to the Graduate Program in Cultural Studies in conformity with the requirements for the Degree of Doctor of Philosophy Queen’s University Kingston, Ontario, Canada June 2016 Copyright © Ian Alexander Cuthbertson, June 2016 Abstract In this thesis I argue that dominant ways of imagining modernity constitute a modern imaginary that carries with it particular expectations concerning modern...»

«CROSS-LINGUISTIC COMPARISON OF RHYTHMIC AND PHONOTACTIC SIMILARITY A DISSERTATION SUBMITTED TO THE GRADUATE DIVISION OF THE UNIVERSITY OF HAWAI‘I AT MĀNOA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY IN LINGUISTICS DECEMBER 2013 By Diana Stojanović Dissertation Committee: Ann M. Peters, Chairperson Patricia Donegan Victoria Anderson Kamil Ud Deen Kyungim Baek © 2013, DIANA STOJANOVIĆ ii ACKNOWLEDGEMENTS I would like to express my deepest gratitude to...»

«Imperial College London Department of Chemical Engineering A Study of Fundamentals in Emulsion Templating for the Preparation of Macroporous Polymer Foams By Dipl.-Chem. Nadine Graeber A dissertation submitted to Imperial College London in fulfilment of the requirements for the degree of Doctor of Philosophy and the Diploma of Membership of Imperial College London September 2013 -i-iiDeclaration I, hereby, certify that the work presented in this dissertation is the result of my own...»

«ARP2/3 COMPLEX HAS A NEUROPROTECTIVE ROLE AND IS REQUIRED FOR MATURE DENDRITIC SPINE HEAD MORPHOLOGY A DISSERTATION SUBMITTED TO THE FACULTY OF THE GRADUATE SCHOOL OF THE UNIVERSITY OF MINNESOTA BY MARCELA MALDONADO IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY LORENE M. LANIER AUGUST 2010 © Marcela Maldonado August 2010 Acknowledgements I would like to thank my committee members, Lorene Lanier, Paul Letourneau, Dezhi Liao, and Lihsia Chen for their support...»

«Cambridge University Press 978-0-521-87347-5 The Cambridge Companion to Epicureanism Edited by James Warren Excerpt More information james warren Introduction Philosophy, as long as a drop of blood shall pulse in its world-subduing and absolutely free heart, will never grow tired of answering its adversaries with the cry of Epicurus: ‘The truly impious man is not he who denies the gods worshipped by the multitude, but he who affirms of the gods what the multitude believes about them’. Karl...»

«Top ten blogs November 2015 by Bart Nooteboom 19. Beyond nihilism: Imperfection on the move published 10-8-2012 The philosopher Nietzsche dealt a death blow to belief in old absolutes, raising the spectre of nihilism. God is dead, and truth, morality and beauty have become subjective, relative and evanescent. There is weak nihilism: regretful loss of belief, and strong nihilism: no longer seeing such belief as desirable. Could we not see the loss of old absolutes as a discarding of shackles, an...»

«LIBERTY UNIVERSITY TO THE JEW FIRST: A SOCIO-HISTORICAL AND BIBLICAL-THEOLOGICAL ANALYSIS OF THE PAULINE TEACHING OF ‘ELECTION’ IN LIGHT OF SECOND TEMPLE JEWISH PATTERNS OF THOUGHT A DISSERTATION SUBMITTED TO THE FACULTY OF LIBERTY BAPTIST THEOLOGICAL SEMINARY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY BY ANTHONY CHADWICK THORNHILL LYNCHBURG, VIRGINIA JUNE 2013 Copyright 2013 A. Chadwick Thornhill All Rights Reserved ii APPROVAL SHEET TO THE JEW FIRST:...»





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