FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:     | 1 |   ...   | 15 | 16 || 18 | 19 |   ...   | 22 |

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

-- [ Page 17 ] --

In contrast, almost all of the other cases of the concurrent step relation do context switch. The context switch relation, CSwitch (S) = S ′, handles all of the details of performing a context switch by removing the head of the schedule (thus allowing the next thread to execute) and aging all of the worlds.

Thread exit (cstep-texit) does not remove the thread from the list, but scheduling a terminated thread simply results in a context switch.

As explained in chapter 4, we do not reason about the resources that threads free (or fail to free) on termination, so we do not place any restrictions on φ.

Figure 8.4 contains the portion of the step relation that is responsible for executing the fully-concurrent statements.

Three rules describe lock acquisition. Rule cstep-prelock checks to make sure that the location that the thread is attempting to lock is a lock in the thread’s resource map and then changes the thread’s status from runnable (Krun) to waiting on a lock (Klock). Finally, cstep-prelock context switches to give other threads a chance to grab the lock first.

Rule cstep-nolock is the “block” case of a blocking lock—we try to grab the lock, but it is not yet available. In this case we simply context switch.

–  –  –

the resource map of the thread. By the restrictions on the lock pool contained in the consistant machine state, this resource map satisfies the lock’s resource invariant4. Rule cstep-lock does not context switch after grabbing the lock. If we wished to context switch here it would not be difficult to modify our proofs; however it is unnecessary (since we quantify over all schedulers) and so we do not do it. See section 5.3 for a further discussion of interleaving.

The cstep-unlock rule reverses the lock rule. It flips the memory location associated with the lock from a 0 to a 1 and puts the resource map associated with the lock φlock into the lock pool L. It is able to uniquely identify this resource map due to the premise

–  –  –

since tightly P is tight, and therefore precise. Since P is an arbitrary predicate in (classical) logic, this premise makes our semantics nonconstructive, i.e., noncomputable. See section 8.6 for further discussion of why this abstraction is reasonable.

In the Coq development we use a different premise, (ρ, φlock, m) |= ⊲ tightly P, The invariant is satisfied on all more approximate resource maps due to the way YES inversion works. To establish that it holds at the current level of approximation is impossible in the general case, but in the case that actually occurs in the proof of the lock rule of CSL, a complex induction is able to prove that it holds immediately.

Perhaps a modification of this rule would somehow lead to a simpler proof of the CSL lock rule.


which is related to the ⊲ discussed in 8.4.6. When we remove the ⊲ there we can simultaneously remove the ⊲ in the cstep-unlock rule.

Finally, cstep-fork creates a new thread. Because we spawn functioncalls as opposed to arbitrary commands that might have free C-minor variables, we don’t need complex side-conditions on free variables and

can use the empty environment ρ0 in the new thread. There is a nonconstructive test that the function’s precondition is satisfied:

(marshal(v), φchild, m) |= validly precisely P.

In this test the parameters of the function call are marshaled into a local environment ρ so that the predicate will be able to judge them. Like the unlock rule, this test is nonconstructive. The sequential semantics does not need such a test at every function call; we need it here to know what world is transferred by the (precise) predicate P that is the function’s precondition. Preconditions of nonspawnable (ordinary) functions need not be precise.

8.6 Reasonableness of the step relation Our semantics has two features that are unusual in a concurrent semantics. The first unusual feature, exhibited in the cstep-seq and cstep-lock rules, is that the semantics does not interleave at every instruction. We discussed this feature in section 5.3.

–  –  –

tests in the cstep-unlock and cstep-fork rules. If we are executing a program for which we have a proof in CSL, then we can prove that the test will always succeed. However, the presence of these nonconstructive tests is unsatisfying. More generally, the presence of resource maps in the semantics is worrying: we need to verify that they are not allowing unrealistic behavior. We can defend both the nonconstructive tests and the presence of resource maps in the semantics by relating our semantics to the erased semantics defined in chapter 5.

The erased machine defined in chapter 5 is similar to the unerased machine defined in this chapter; the difference is that in the erased machine all of the resource maps have been removed. The unerased machine is actually a conservative approximation to the erased one, as

demonstrated by the erasure theorem:

Theorem (Erasure). If Ψ ⊢ (℧, θ, L, φmp, φfp, m) =⇒

–  –  –

Proof. By case analysis on the =⇒ relation. We observe that each case in that relation has a corrosponding case in the =⇒e relation with a subset of the premises. In each case the schedule, locals (inside a thread), concurrent controls (inside a thread), thread list (up to erasure), and memory are identical. For the cstep-seq case we use lemma 8.2.

This is a useful sanity check: the real machine takes no decisions


based on erasable information; the erased semantics simply gets stuck less often.

When to erase. One could imagine proving safety of a concurrent program with respect to the unerased semantics, then erasing, and last compiling. However, this would be a mistake since the compiler may do concurrency-unsafe optimizations. Instead, we should preserve the resource maps in the semantics of each intermediate representation as we compile from Concurrent C minor to machine language; this gives the compiler a specification of concurrency-safe optimizations. After we have reached machine language, we can use the resource maps to prove that our interleaving model is sound for machines with weak memory models. We erase last.

–  –  –

We have now given a formal concurrent operational semantics for Concurrent C minor. This semantics isolates the behavior of the sequential step relation from the concurrent reasoning, making it easy to use to reason about concurrent features such as locking a lock. However, it is not a major goal to use our operational semantics to reason about the sequential features of Concurrent C minor. To do so we define an oracular semantics for Concurrent C minor in chapter 9.

Chapter 9 Oracle Semantics In chapter 3 we introduced Concurrent C minor, and in chapter 8 we gave it a formal concurrent operational semantics. That semantics allows for natural reasoning about the fully concurrent operations of Concurrent C minor, such as lock and unlock. However, it does not allow for natural reasoning about the sequential language features such as control flow. In this chapter we define an oracular semantics for Concurrent C minor that is ideal for reasoning about sequential language features in the context of a concurrent program1.

–  –  –

A compiler, or a Hoare tuple, considers a single thread at a time. The compiler (and its correctness proof) wants to compile code uniformly even around the concurrent operations. Similarly, in a CSL proof, the Portions of this chapter have been published before as [HAZ08a] and [HAZ08b].

–  –  –

may contain concurrent operations, but, because of C minor’s nonlocal exits, a soundness proof for the sequence rule of separation logic is complicated even without the headaches of concurrency. We want a semantics of single-threaded computation in a concurrent context.

The sequential submachine of section 8.2 is single-threaded but incomplete because it gets stuck at the fully-concurrent operations lock, unlock, and fork. What we want is a deterministic sequential operational semantics2 that knows how to handle concurrent communications, which it will do by consulting an oracle.

The correctness proofs of the CompCert compiler and the sequential separation logic proofs use determinism to simplify their task.

9.1. WHY AN ORACULAR SEMANTICS  Figure 9.1 demonstrates the value of this type of semantics. In the left column is a sequence of statements in Concurrent C minor. The first two statements are sequential statements, the third is a fully-concurrent lock statement, and the final statement is sequential. In the middle column is a series of states σ (i.e., memory, locals, etc.) from a sequential semantics such as the sequential submachine; the series starts with some initial state σ0. In the right column is a series of oracle Ω and state σ pairs for a new oracular semantics; we start with the same state σ0 as in the regular sequential semantics, as well as some intitial oracle Ω0.

As each statement is executed, the states in the middle and right columns are updated by the action of the statement. After executing the first statement, which is a store to memory, in the middle column we have a new state σ1. In the right column, we get exactly the same state σ1. Since a store instruction is not a concurrent instruction, we do not use the oracle and so it is unchanged. Assuming that the substatements s1 and s2 do not contain concurrent instructions, we reach the subsequent state σ2.

Now we reach a concurrent statement, lock. Here, the standard sequential semantics is stuck; the sequential submachine is not able to determine the result of the lock instruction, since it depends on the other threads. However, on the right-hand side, the semantics is able to take advantage of the oracle Ω0. The oracle represents all of the other threads in the concurrent machine. The right-hand semantics consults the oracle, which predicts what the state σ3 will be after the concurrent


 machine executes the lock instruction, and also produces a new oracle Ω1, which will be usable for the next concurrent instruction. After the concurrent instruction, the right-hand side is able to continue to process sequential statements as before.

To build the desired semantics we will build an oracular machine using our extension system explained in chapter 6. Our extension will handle all of the concurrent instructions of Concurrent C minor.

–  –  –

Like any extension, we must define the type of an oracle and build a partial function consult. When we constructed the sequential submachine in section 8.2, we used the unit oracle. Here, we define a more

meaningful oracle as follows:

–  –  –

thread number i, we first split the alloc and function pools from the resource map φ, leaving the remaining resource map φt. The predicate allocpool is precise, and the function pool contains all of the functions and nothing more, so splitting them off is deterministic. Next we can

–  –  –

9.3 Concurrent consult relation We need to build a consult relation to execute the concurrent statements of Concurrent C minor. The consult function constructs a concurrent machine S from the oracle and then runs the other theads in that machine until control returns.

We run the other threads with the StepOthers relation, defined in figure 9.3. The StepOthers relation takes a thread-ID i and two concurrent machine states S and S ′. We say that thread i is ready when i is at the head of the schedule in S. When we step other threads we have two choices. The first case, SO-done, says that if thread i is ready, then we have finished stepping other threads and control has returned to thread i. The second case, SO-step, says that if thread i is not ready, then we take a step in the concurrent machine and then test again.

–  –  –

when the oracular machine wants to consult.

In the first case, Ω-invalid, there is no concurrent machine state S compatible with the concurrent continuation. This happens if the oracle Ω is somehow incompatible with the world w. There are a variety of ways that this could be the case; one simple example is that one of the threads inside the oracle thinks that it has full ownership of a location that is also owned by the world w. Of course, in the concurrent machine this is forbidden by the consistency requirements.

It our proofs it is convienent to quantify universally over all oracles, instead of of simply quantifying over valid oracles, which would require an additional premise in the definitions and proofs. By looping safely if


 we are handed an invalid oracle by the universal quantification, we can gracefully handle invalid oracles without requiring such a premise. By returning None from the consult function we indicate that the semantics should loop endlessly, thereby trivially becoming safe.

In the remaining two cases, we are able to construct a concurrent machine S, and take at least one concurrent step. This step uses the cstep-seq case in the concurrent step relation to execute a make lock or free lock, uses cstep-prelock to execute the first part of a lock, uses cstep-unlock to execute an unlock, or uses cstep-fork to execute a fork.

After taking this step, the machine decides (classically) whether control will return to the current thread by branching on the StepOthers judgement. Rule Ω-diverges handles the case when control does not return, for example if the schedule is unfair, if another thread executes an illegal instruction, or if the current thread is deadlocked. In these cases the oracle machine loops endlessly, thereby becoming trivially safe. The idea that we are safe if another thread blows up may seem strange: the point is that we are proving the safety of this thread. If another thread causes the concurrent machine to get stuck, it is not this thread’s fault.

Pages:     | 1 |   ...   | 15 | 16 || 18 | 19 |   ...   | 22 |

Similar works:

«TEXTUAL PROJECTIONS: THE EMERGENCE OF A POSTCOLONIAL AMERICAN GOTHIC By ROBERT C. SCHACHEL A DISSERTATION PRESENTED TO THE GRADUATE SCHOOL OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY UNIVERSITY OF FLORIDA 2006 Copyright 2006 by Robert C. Schachel To my father ACKNOWLEDGMENTS I thank my committee chair and mentor, Dr. David Leverenz, for all of his encouragement, support, insight, and academic guidance over the past eleven years....»

«Isabelle Labonté MUSCLE LISSE BRONCHIQUE ET ASTHME Etudes in vivo et in vitro Thèse présentée à la Faculté des études supérieures de l'Université Laval dans le cadre du programme de doctorat en médecine expérimentale pour l'obtention du grade de Docteur es Philosophia (PhD) Département de médecine expérimentale Faculté de médecine Université Laval Québec 2009 © Isabelle Labonté, 2009 II Résumé Les cellules musculaires lisses (CML) jouent un rôle primordial dans la...»

«1 A Framework for the Characterization and Analysis of Software Systems Scalability Ana Leticia de Cerqueira Leite Duboc Thesis submitted for the degree of Doctor of Philosophy of UCL Department of Computer Science University College London 2009 2 I, Ana Leticia de Cerqueira Leite Duboc, confirm that the work presented in this thesis is my own. Where information has been derived from other sources, I confirm that this has been indicated in the thesis. Abstract 3 Abstract The term scalability...»

«Inference of computational models of tendon networks via sparse experimentation by Manish Umesh Kurse A Dissertation Presented to the FACULTY OF THE USC GRADUATE SCHOOL UNIVERSITY OF SOUTHERN CALIFORNIA In Partial Fulfillment of the Requirements for the Degree DOCTOR OF PHILOSOPHY (BIOMEDICAL ENGINEERING) June 2012 Copyright 2012 Manish Umesh Kurse ii Dedication To my parents. iii Acknowledgements Little did I know when I started my Ph.D. that this journey I was about to undertake would teach...»

«Community Cellular Networks by Kurtis Heimerl 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 Eric Brewer, Co-chair Assistant Professor Tapan Parikh, Co-chair Associate Professor Jenna Burrell Professor Ali Niknejad Fall 2013 Community Cellular Networks Copyright 2013 by Kurtis Heimerl Abstract Community Cellular...»

«Magneto-Optic Polymers and Devices Item type text; Electronic Dissertation Authors Lopez Santiago, Alejandra Publisher The University of Arizona. Rights Copyright © is held by the author. Digital access to this material is made possible by the University Libraries, University of Arizona. Further transmission, reproduction or presentation (such as public display or performance) of protected items is prohibited except with permission of the author. Downloaded 16-Nov-2016 04:00:06 Link to item...»

«Monstrosity in Literature, PsychoanaLysis, and PhiLosoPhy edited by Gerhard unterthurner and erik M. Vogt Verlag Turia + KanT Wien – Berlin Bibliografische Information der Deutschen Nationalbibliothek Die Deutsche Bibliothek verzeichnet diese Publikation in der Deutschen Nationalbibliografie; detaillierte bibliografische Daten sind im Internet über http://dnb.ddb.de abrufbar. Bibliographic Information published by the Deutsche Nationalbibliothek The Deutsche Bibliothek lists this publication...»

«The Impact of Revenue Diversification on the Financial and Educational Outcomes of Private Colleges and Universities during the Great Recession by James C. Webb A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Higher Education) in the University of Michigan 2014 Doctoral Committee: Professor Edward P. St. John, Chair Associate Professor Emeritus Richard L. Alfred Professor Brian P. McCall Assistant Professor Larry L. Rowley...»

«The effect of contamination on selected physical and chemical characteristics of Mineral Trioxide Aggregate Thesis submitted in fulfilment of the degree of Doctor of Philosophy Mohammad Hossein Nekoofar School of Dentistry Cardiff University (April 2006-August 2011) DECLARATION This work has not previously been accepted in substance for any degree and is not concurrently submitted in candidature for any degree. Thursday, 23 June 2011 STATEMENT 1 This thesis is being submitted in partial...»

«Stony Brook University The official electronic file of this thesis or dissertation is maintained by the University Libraries on behalf of The Graduate School at Stony Brook University. © Allll Riightts Reserved by Autthor. © A R gh s Reserved by Au hor Neural Mechanisms of Selective Auditory Attention in Rats A Dissertation Presented by Lung-Hao Tai to The Graduate School in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy in Neuroscience Stony Brook University...»


«THOU ART UNREAL, MY IDEAL: NOSTALGIA AS IDEOLOGY IN THE NOVELS OF EVELYN WAUGH, ALDOUS HUXLEY AND GEORGE ORWELL By ZACHARY E. SHOWERS A DISSERTATION Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in the Department of English in the Graduate School of The University of Alabama TUSCALOOSA, ALABAMA 2010 Copyright Zachary Elijah Showers 2010 ALL RIGHTS RESERVED ABSTRACT The satirical novels of Evelyn Waugh, Aldous Huxley and George Orwell share a sense...»

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