FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:     | 1 |   ...   | 9 | 10 || 12 | 13 |   ...   | 22 |

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

-- [ Page 11 ] --

129 (* See section 6.XX *) 131 Axiom step_allocpool: forall ge st st’, 132-134 (* See figure 5.8 *)

–  –  –

(lines 118–119); the other possibility (lines 104–111 and 120) is related to the C minor memory model and is covered in section 6.3.2.

The axiom step fun on lines 124–125 says that the step relation must be deterministic. This property is heavily used in both the CompCert compiler proofs and the soundness proofs of sequential separation logic developed by Appel and Blazy.

The axiom step not any younger is a technical axiom required by the model of resources, resource maps, and predicates, and will be explained in chapter 7.

6.3.2 Definitions and axioms for the C minor

–  –  –

Here we give a brief explanation of some definitions and axioms required by the CompCert memory model; Leroy et al. [LB08, Ler06] give a fuller explanation of the memory model and the reasons behind its design decisions.

The resource RESERVED is used to indicate memory locations that have not been allocated, but can be allocated in the future. The resource CT is used because C minor is byte-addressed; accordingly, since locks are four bytes long, the first byte has resource LK and the next three have resource CT.

–  –  –

104 (* Required for CompCert memory model *) 105 Definition rmap_memory_model_rmap_ok (phi phi’:rmap) := 106 forall addr, 107 (phi @ addr = RESERVED phi pfullshare /\ 108 ((phi’ @ addr = VAL phi’ pfullshare) \/ 109 (phi’ @ addr = NO phi’))) \/ 110 (phi @ addr = VAL phi pfullshare /\ 111 phi’ @ addr = NO phi’).


131 Axiom step_allocpool: forall ge st st’, 132 step ge st st’ allocpool * TT) (filter ge st) allocpool * TT) (filter ge st’)).

–  –  –

The definition rmap memory model rmap ok on lines 104–111 gives two additional ways the resource map is able to change. In the first, on lines 107–109, resource is allowed to change from RESERVED to VAL or NO; this happens when memory is allocated. In the second, on lines 110–111, resource is allowed to change from VAL to NO; this happens when memory is deallocated.

The axiom step allocpool on lines 131–134 is an elegant way of expressing that one never “runs out” of allocatable memory. Instead of expressing this fact directly, the axiom is defined in terms of a predicate allocpool, which must be a satisfied by some portion of the resource map (TT is the predicate true). The definition of allocpool is both technical and not relevant to concurrency, and so we do not present it here.


 135 Inductive stepstar (ge:genv): state- state- Prop := 136 | stepstar_0: forall st, 137 stepstar ge st st 138 | stepstar_S: forall st1 st2 st3, 139 step ge st1 st2 stepstar ge st2 st3 stepstar ge st1 st3.

143 Inductive immed_safe (ge : genv) (st: state) : Prop := 144 | immed_safe_step: forall st’, 145 step ge st st’ immed_safe ge st 147 | immed_safe_rmap:

148... level of resource map is 0; see chapter 6... immed_safe ge st.

151 Definition safe (ge: genv) (st: state) : Prop := 152 forall st’, stepstar ge st st’ - immed_safe ge st’.

Figure 6.7: Basic definitions for Extensible Semantics 6.

3.3 Common definitions for core semantics Finally, there are some common definitions for all core semantics which are given in figure 6.7. stepstar is defined in the standard inductive way to allow for finite composed applications of step. On lines 144–146, immed safe says that a state is immediately safe if it can take a step; on lines 147–149 there is an additional way to be immediately safe, which is if the “level” of the resource map in the state is 0; this is required for the model of resource maps and will be explained in chapter 7.

–  –  –

6.4 Building an extension Once we have a core language, such as the C minor of Appel and Blazy, we want to extend it, for example with concurrency primatives. By using a “bolt-on” model for extensions, we can ensure that changes to the core semantics do not affect the extensions and vise versa.

6.4.1 Examples of extensions Here we discuss different examples of extensions definable in our setting.

The null extension One very simple extension is the null extension, which is the extension that does not implement any functionality. In this case the combination of the core language and the extension is equivalent to just the core language.

The operating system extension A more complex extension is the simple operating system extension.

This extension implements three external functions: read, which gets input from the user; write, which sends output to the user; and exit, which terminates the program and returns control to the operating system.


 The sequential sub-machine extension To define the semantics of Concurrent C minor we will build two different concurrency extensions. In chapter 8, we will build a small extension called the sequential sub-machine extension that only knows how to execute the concurrent instructions make lock and free lock, getting stuck on lock, unlock, and fork. We will use this extension to build the concurrent operational semantics of Concurrent C minor.

The oracular concurrency extension Later, in chapter 9, we will build a more powerful extension using the concurrent operational semantics, called the oracular concurrency extension. That extension will be able to execute all five of the concurrent instructions, and we will use it to prove our CSL sound.

6.4.2 The EXTENSION module type An extension must satisfy the module type given in figure 6.8. Unlike the core, extensions are quite simple. There is a type oracle (in mathematical notation Ω), which acts as “private data” for the extension and is hidden from the core semantics. The oracle type must be inhabited, so we provide a witness, an oracle.

The point of an extension is to handle external function calls. However, any given extension need not handle all external functions; it is useful to be able to query the extension to determine which external functions it handles. The parameter handles gives an easy test for this.


156 Parameter oracle: Type.

157 Parameter an_oracle: oracle.

159 Parameter handles: external_function - bool.

161 Parameter consult: external_function oracle * world * predicate) option (oracle * world) - Prop.

165 Axiom consult_obeys_rmap: forall c o1 w1 P o2 w2, 166 consult c (o1, w1, P) (o2, w2) match (w1,w2) with ((_,_,rmap,m),(_,_,rmap’,m’)) = 168 forall addr, (readable (rmap @ addr) /\ 169 readable (rmap’ @ addr)) m addr = m’ addr)) 171 end.

173 (* Determinism *) 174 Axiom consult_fun: forall c a b1 b2, 175 consult c a b1 - consult c a b2 - b1=b2.

177 (* Required for model of resource maps *) 178 Axiom consult_not_any_younger:

179 (* See section 6.XX *) 181 (* Required for CompCert memory model *) 182 Axiom consult_allocpool: forall c ora w P ora’ w’, 183 consult c (ora, w, P) (Some (ora’, w’)) allocpool * TT) w allocpool * TT) w’).


Figure 6.8: Interface for extension



 To actually handle the external function call, the extension provides a consult relation, which takes an external function (i.e. a natural number that encodes which function is being called), a tuple (Ω, w, P ), which are the arguments to the external call, and an option of tuple (Ω, w), which are the results.

In general, consult only modifies world, since world is exactly the part of the state that is shared between all of the languages of the CompCert compiler. However, the extension is allowed to use some auxiliary private state in the oracle. In the operating system extension this would encapsulate the state of the operating system; in the oracular concurrency extension it encapsulates the state of the other threads.

The predicate P in the consult function is used to implement make lock. It would also be useful to implement an assert function that took a predicate instead of an expression.

Like step, the consult relation is partial and can get stuck. When consult returns None, the result is not that the consult failed, but that control never returns. Two examples of this result would be modeling the exit system call in the operating system extension and modeling the lock instruction, where e.g. the call can deadlock, in the oracular concurrency extension. When consult returns a new oracle and world, the world is passed back to the core semantics and the oracle is provided as a parameter on the next consult, thereby allowing the extension to use the oracle as shared state. In general the oracle is able to return a completely different world (memory, resource map, etc.) than the one


In addition, like the core semantics, an extension must satisfy a variety of axioms10. The key axiom is consult obeys rmap, which is given on lines 165–171. This axiom is somewhat different from the one defined for the core on lines 96–102 in figure 6.5. Instead, this one guarantees that as long as an address is readable both before and after consulting then the memory at that address is unchanged by the consult.

All of the other axioms are very similar to the ones given for the core in figures 6.5 and 6.6.

6.5 Gluing a core and extension together Once one has built a core semantics and an extension, one would like to glue them together to have a complete semantics. We define a functor Oraclize in Coq that takes two modules as arguments, the first of module type EXTENSIBLE SEMANTICS, and the second of module type EXTENSION. This functor then builds a step relation of the following

–  –  –

The Coq implementation of the oracular step relation is in figure 6.9.

The oracular step has three cases. Case one is given on lines 4–8.

First, in line 5 we ensure that the state is not at an external function Just as with the core axioms, it has been shown in Coq that the concurrency extension meets these axioms, but it is unclear if other axioms are required as the proof is being re-engineered into this format.


 Module Oraclize (Core: EXTENSIBLE_SEMANTICS) (Ext: EXTENSION).


1 Inductive oracle_step 2 (ge: genv) (ora1 : oracle) (st1 : state) 3 (ora2: oracle) (st2: state) : Prop := 4 | step_core:

5 at_external (snd (snd (from_state st1))) = None ora1 = ora2 - 7 step ge st1 st2 - 8 oracle_step ge ora1 st1 ora2 st2 9 | step_external_Some:

10 forall phi m core f vargs P rho’ rho’ core’, 11 st1 = to_state (phi, m, core) at_external core = Some (f,vargs,P) consult f (ora1,(snd ge,vargs,phi,m), P) 14 (Some (ora2,(_,rho’,phi’,m’))) after_external rho’ core = Some core’ st2 = to_state (phi’,m’,core’) oracle_step ge ora1 st1 ora2 st2 18 | step_external_None:

19 forall phi m core f vargs P, 20 st1 = to_state (phi, m, core) at_external core = Some (f,vargs,P) consult f (ora1,(snd ge,vargs,phi,m),P) None ora1 = ora2 - 24 st1 = st2 - 25 oracle_step ge ora1 st1 ora2 st2.


End Oraclize.

–  –  –

call; in this case line 6 ensures that the oracle is constant since the core semantics is not allowed to modify the it. On line 7, the core semantics steps, and on line 8 the parts are put back together.

Both cases two and three deal with external function calls. Case two is given on lines 9–17, and handles the case when the external function returns. We verify that the state is at an external function call on line

12. On lines 13–14, we consult the oracle using the extension. After consulting we reconstruct the state on lines 15–16, and on line 17 the parts are put back together.

Case three is given on lines 18–25 and handles the case when the external function never returns control. We verify that the state is at an external function call on line 21. On line 22, we consult the oracle using the extension, and receive None back as the return, indicating that the extension never releases control back to the core. In this case, the semantics loops around forever by setting the next state and oracle to be equal to the previous one on lines 23–24, and then putting the parts back together on line 25. Since the third case results in an infinite loop, it is trivially safe.

Along with this definition, the Oracalize functor has a number of lemmas about the relation, which are proven from the axioms on the core and extension.



6.6 Notation for the rest of the thesis We have now given an explanation of how to modularize an extensible semantics in Coq. To simplify the presentation in the rest of the thesis, we will do the following. First, we will assume that the core semantics is “hardwired” to the C minor of Appel and Blazy. The core semantics will have a step relation given by

–  –  –

Where a state σ is a pair of world w (that is, those parts of state that do not include program syntax: locals ρ, resource map φ, and memory m) and control κ (the parts of the state that do include program syntax).

Appel and Blazy define several different controls, but for this presentation we only s · κ and Kstop, as defined in chapter 5.

Second, we will pretend that the new concurrent statements make lock, free lock, lock, unlock, and fork are just normal statements added to sequential C minor, instead of extended function calls. These statements take values instead of expressions as parameters for simplicity.

Third, we will hide most of the modularization between core and extension. To build an extension, one constructs a partial function consult:

consult : program × oracle × state → option(oracle × state),

–  –  –

consultation, and an oracle Ω′ and state σ ′ are the optional output.

Pages:     | 1 |   ...   | 9 | 10 || 12 | 13 |   ...   | 22 |

Similar works:

«About Heidegger’s call of conscience Cristóbal Holzapfel 1 By Heidegger the conscience is conceived as a call (Ruf). This is framed within the question about a being-a-whole1 (Ganzsein). If the Dasein (human being), conceived in the I Section of Sein und Zeit, Being and time (in the following ‘Bat’) was understood especially as the Dasein between birth and death, within the Existential Analytic being and time have stayed out. What referes to the relationship from Dasein to deatth will...»

«SECONDARY CIRCULATION IN A SINUOUS COASTAL PLAIN ESTUARY A Dissertation Presented to The Academic Faculty By Susan Anne Elston In Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy in Earth and Atmospheric Sciences Georgia Institute of Technology May 2005 Copyright © 2005 by Susan Anne Elston SECONDARY CIRCULATION IN A SINUOUS COASTAL PLAIN ESTUARY Approved by: Dr. Jackson O. Blanton, Advisor Dr. Judith A. Curry Skidaway Institute of Oceanography School of Earth &...»

«De se preferences and empathy for future selves1 L.A. Paul To be published in Philosophical Perspectives (Metaphysics: 2017), eds. John Hawthorne and Jason Turner. Abstract: I argue that we grasp distinctive, self-involving truths, or de se truths, through immersive experience. Drawing on examples involving gameplay and virtual reality, I defend the value of immersive exploration and virtual first personal perspectives, and explore the relation between a virtual first personal perspective and a...»

«REFRAMING OUR UNDERSTANDING OF NONPROFIT REGULATION THROUGH THE USE OF THE INSTITUTIONAL ANALYSIS AND DEVELOPMENT FRAMEWORK by Denise R. Vienne A Dissertation Submitted to the Faculty of The College for Design and Social Inquiry in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy Florida Atlantic University Boca Raton, Florida August 2014   Copyright Denise R. Vienne 2014   ii ACKNOWLEDGEMENTS This dissertation, not to mention the coursework, comprehensive...»


«BOSTON UNIVERSITY GRADUATE SCHOOL OF ARTS AND SCIENCES Dissertation THE STRUCTURE OF DETERMINER PHRASES: EVIDENCE FROM AMERICAN SIGN LANGUAGE by DAWN MacLAUGHLIN B.S., Massachusetts Institute of Technology, 1986 Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy © Copyright by DAWN MacLAUGHLIN Approved by First Reader Carol Neidle, Ph.D. Associate Professor of Linguistics Boston University Second Reader Judy Anne Kegl, Ph.D. Research Assistant Professor...»

«Dissertation for the degree philosophiae doctor (PhD) at the University of Bergen Dissertation date: ACKNOWLEDGEMENTS ABSTRACT LIST OF PUBLICATIONS ABBREVIATIONS 1 INTRODUCTION 1.1 Gliomas 1.1.1 Classification and grading 1.1.2 Incidence and prognosis 1.1.3 Conventional therapies 1.1.4 Challenges associated with the treatment of GBMs 1.2 Anti-angiogenic therapy 1.2.1 Anti-angiogenic compounds 1.2.2 Response to anti-angiogenic therapy and adaptation mechanisms 1.3 Modalities for the imaging of...»

«The Concept of the Ascent of Prayer by Sixteenth-century Jerusalem Kabbalist, R. Joseph ibn Zayyah Thesis submitted for the degree of “Doctor of Philosophy” by Sachi Ogimoto Submitted to the Senate of the Hebrew University of Jerusalem August 2011 This work was carried out under the supervision of Professor Jonathan Garb Acknowledgements First and foremost, I would like to express my deep and sincere gratitude to my supervisor, Professor Jonathan Garb, of the Department of Jewish Thought,...»

«Design of Nanostructured Ag Catalysts for Selective Heterogeneous Catalytic and Photocatalytic Oxidation Reactions by Phillip Neil Christopher A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Chemical Engineering) in The University of Michigan Doctoral Committee: Associate Professor Suljo Linic, Chair Professor Phillip E. Savage Professor Johannes W. Schwank Assistant Professor Anton Van Der Ven © Phillip Neil Christopher This...»

«379 yva/j M0e 3mg AMBIGUITY OF LOSS, ANTICIPATORY GRIEF, AND BOUNDARY AMBIGUITY IN CAREGIVER SPOUSES AND PARENTS DISSERTATION Presented to the Graduate Council of the University of North Texas in Partial Fulfillment of the Requirements For the Degree of DOCTOR OF PHILOSOPHY by Jan K. Rider, B.F.A., M.S. Denton, Texas August, 1993 yva/j M0e 3mg AMBIGUITY OF LOSS, ANTICIPATORY GRIEF, AND BOUNDARY AMBIGUITY IN CAREGIVER SPOUSES AND PARENTS DISSERTATION Presented to the Graduate Council of the...»

«Molecular-scale Organic Electronic Devices for Integrated Nonvolatile Memory Application Troy Graves-Abe A DISSERTATION PRESENTED TO THE FACULTY OF PRINCETON UNIVERSITY IN CANDIDACY FOR THE DEGREE OF DOCTOR OF PHILOSOPHY RECOMMENDED FOR ACCEPTANCE BY THE DEPARTMENT OF ELECTRICAL ENGINEERING JUNE 2006 © Copyright 2006 by Troy Graves-Abe All rights reserved. Abstract Self-assembly techniques that allow the controlled growth of nanometer-scale organic molecular films present new opportunities to...»

«NOTE TO USERS This reproduction is the best copy available. UMI° Creaturely Pleasures: The Representation of Animals in Early Modern Drama Yael Margalit August 2008 Department of English McGill University, Montreal A thesis submitted to McGill University in partial fulfillment of the degree of Doctor of Philosophy. © Yael Margalit 2008 1*1 Library and Archives Bibliotheque et Archives Canada Canada Published Heritage Direction du Branch Patrimoine de I'edition 395 Wellington Street 395, rue...»

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