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



Pages:     | 1 |   ...   | 8 | 9 || 11 | 12 |   ...   | 22 |

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

-- [ Page 10 ] --

World, Predicate. We call the tuple of globals, locals, resource map, and memory a world. A predicate is a function from a world to a proposition in the calculus of co-inductive constructions (Coq’s Prop). All of the assertions of separation logic developed in chapter 4 are predicates. A major advantage of defining things in this way is that since all of the components in a world are level-independent, so are predicates. Therefore, all of our separation logic assertions are welldefined and indeed have the same definition for all of the languages in CompCert.

External functions. Finally, one of the few statement types that is shared by all of the CompCert languages is the idea of an external function call, such as a library call, trap to the operating system, or other similar situation. Each external function is given a unique identier, and a global table maps identifiers to the proper calling convention at each level in the compiler. There is therefore a uniform way to represent external function calls for all CompCert languages, and we will use this infrastructure to build our extension system.

CHAPTER 6. ENGINEERING ISOLATION

 6.2.2 Resource maps Informally, a resource map, like the footprint of Appel and Blazy, is a map from an address to a permission, which we call a resource. As in Appel and Blazy’s setting, using memory without the correct permission causes the machine to get stuck.

The formal definition of resource maps is technical and will be covered in chapter 7. In figure 6.3 we present an “axiomatic” view of the core definitions.

As explained above, a resource is a kind of permission, and a resource map is a function from addresses to resources. Given a resource map rm one uses resource at to determine the resource at a given address addr. Since this is the primary use for a resource map, we define

the notation @; this means:

–  –  –

A nonempty fractional share, as defined in section 4.5, has type pshare.

Resources have a kind, which is an inductive type that has five constructors: kVAL (regular data), kFUN (functions), kLK (locks), kRES, and kCT. Both kRES, and kCT are related to the C minor memory model and are explained in section 6.3.2.

We provide two pseudoconstructors for building resources: NO and YES. Both take a resource map as the first parameter; the reason for this parameter will be explained in chapter 7. For the purposes of this

6.2. SHARED DEFINITIONS FOR GLUE  21 (* Permissions *) 22 Parameter resource : Type.

24 (* A map from address to permissions *) 25 Parameter rmap : Type.

27 (* How to get from an rmap to a resource *) 28 Parameter resource_at: rmap - address - resource.

29 Infix "@" := resource_at (at level 50,no associativity).

31 (* Fractional ownership - nonempty share *) 32 Parameter pshare : Type.

34 (* Resource kinds *) 35 Inductive kind := 36 kVAL | kFUN | kLK | kRES | kCT.

38 (* Resource

Abstract

pseudoconstructors *) 39 Parameter NO : rmap - resource.

40 Parameter YES : rmap - kind - pshare list predicate) - resource.

43 (* Resource pseudoconstructors *) 44 Definition VAL (rm: rmap) (sh: pshare) := 45 YES rm sh kVAL nil.

46 Definition FUN (rm: rmap)(sh: pshare)(P Q:predicate) := 47 YES rm fullshare kFUN (P :: Q :: nil).

48 Definition LK (rm: rmap) (sh: pshare) (R: predicate) := 49 YES rm sh kLK (R :: nil).

50 Definition RESERVED (rm: rmap) := 51 YES rm fullshare kRES nil.

52 Definition CT (rm: rmap) (sh: pshare) := 53 YES rm sh kCT nil.

–  –  –

chapter, this parameter is not important.

NO rm indicates that all forms of access to that memory location are forbidden5. YES rm k sh LP indicates that the memory location permits certain kinds of access, the exact nature of which is determined by the kind k, share sh and list of predicates LP.

Using YES we define five different resources: VAL, FUN, LK, RESERVED, and CT. VAL rm sh indicates that the location is owned with (positive) fractional ownership sh. Partial ownership will give permission to read from memory; full ownership will give permission to both read from

and write, and so we define readable and writable as:

–  –  –

FUN rm P Q indicates that the address contains a function with precondition P and postcondition Q; in other words, if P is satisfied just before jumping to the address, then Q will be satisfied after the function returns. FUN uses fullshare for its share; we will use a special resource map called the function pool to make sure that all threads have access to the functions6.

LK rm sh R indicates that the address is partially owned with share Another way to think about resource maps is that they are partial functions;

in this case NO rm indicates that the location is not in the domain.

Recall that in section 4.7.3 the CSL function assertion does not have a share.

6.2. SHARED DEFINITIONS FOR GLUE  sh, and contains a lock with associated invariant R; in other words, locking the lock will result in gaining the invariant R. RESERVED rm and RESERVED rm sh are related to the C minor memory model and are explained in section 6.3.2.





There are three important points to note. First, these “constructors” are semantic, meaning that new kinds of resource can be defined at any time; accordingly, if one has a resource, it does not follow that it is one of these five. In fact, the underlying model is strong enough to allow for an open-ended number of resource kinds, although in the Coq development we only have the five explained above.

Second, these pseudoconstructors are not fully invertible; i.e., from:

–  –  –

we can conclude that k = k’ and that sh = sh’; however it is invalid to conclude that rm = rm’ or that LP = LP’; in chapter 7 we will explain exactly what can be concluded about these parameters.

Third, eagle-eyed readers may have noticed that the definition of YES on lines 40–41 takes a list of predicates as parameters, but predicate is not defined until line 59 (in figure 6.2). In general, this is a problem.

The definition of predicate given on line 59 is correct. In chapter 7 we will show that in fact resource, rmap, and predicate are all defined simultainously in a noncircular way. For the purposes of this chapter, we will ignore this issue and therefore remain slightly informal.

CHAPTER 6. ENGINEERING ISOLATION



–  –  –

where Ψ is a global environment (mostly the syntax of the running program) and σ is a state. We require that σ be isomorphic to a tuple of (φ, m, ς), where φ is a resource map, m is the memory, and ς is other kinds of state, such as in C minor the stack pointer, local variables, and control (code, i.e., program syntax). We distinguish the memory and resource map because the types of these are the same in every language in the CompCert stack. Other components of the state are unique to each language and are bundled into the core state ς.

We show the Coq interface axiomatizing these ideas in figure 6.47.

Of course, each language has its own type of syntax, which in the module is called the program. Each language also has its own state, denoted σ, which is isomorphic to a triple of rmap φ, mem m, and core ς. Requiring an isomorphism instead of requiring state to be a triple gives the languages additional flexibility in their definitions. We require that the core contain some represention of local variables.

Extensibility is given by the parameter at external. While the program is executing normal instructions, at external returns None.

When control reaches an external function call it transforms its private Proven in Coq: C minor satisfies the interface.

6.3. AN EXTENSIBLE SEMANTICS  62 Module Type EXTENSIBLE_SEMANTICS.

64 (* Syntax *) 65 Parameter program : Type.

67 (* Level-dependent representation *) 68 Parameter state : Type.

70 (* Level-dependent data *) 71 Parameter core : Type.

73 Parameter from_state : state - rmap * mem * core.

74 Parameter to_state : rmap * mem * core - state.

75 Parameter core_locals: core - locals.

77 Parameter at_external: core option (ext_fun * locals * predicate).

79 Parameter after_external: locals- core- option core.

81 Definition genv: Type := (program * globals).

83 Definition filter (ge: genv) (st: state) : world := 84 match (from_state st) with (rm, m, c) = 85 (snd ge, core_locals c, rm, m) 86 end.

88 (* call main *) 89 Parameter initial_core: val - list val - core.

91 Parameter step: genv - state - state - Prop.

93 (* Axioms about the step relation *) 94-152 (* See figures 5.7, 5.8, and 5.9 *) 154 End EXTENSIBLE_SEMANTICS.

–  –  –

representation of that call into a language-independent representation.

In a language-independent representation, an external function call has three components. First, an identifier that specifies which function call, for example a 0 for lock or a 1 for unlock. Second, a set of locals, which become the parameters to the external function. Finally, external function calls are also able to take a predicate; this is required so that we can handle make lock, which takes a resource invariant (predicate) as a parameter; it would also be useful if one wished to define an assert statement that took a real separation logic assertion instead of an expression.

Once the external function call is in the language-independent representation, an extension is able to provide the proper semantics. The extension is allowed to modify both the resource map and the memory as it executes, but is not allowed to modify the language-dependent core state. When the extension wishes to return control to the core, it places the return value of the function into a locals type and uses the after external parameter to resume the core semantics.

Global data genv, denoted Ψ, is a tuple of two components: a language-depenent program, which contains the syntax of the code, and a language-independent global map, which maps global names to addresses.

Since each language has a different representation of state, the definition filter is provided so that the same predicate can be applied regardless of the details of the current language in the compilation proAN EXTENSIBLE SEMANTICS  cess. To apply the predicate Q in the context of language L1 to the state

σ1 of type L1.state, one writes in Coq:

–  –  –

The ability to use the same predicate Q with different languages should significantly simplify modifications to the compiler, since it means that the compiler will not have to manipulate predicates as it compiles code from one language to the next.

Although the internals of core vary significantly between the languages, all of the languages support the idea of creating an initial, simple core, typically for program start with call main(). The parameter initial core is provided for that purpose.

Most importantly, a language has a step relation (i.e., −→), which gives its actual small-step semantics.

For a given state, there does not always exist a subsequent state that the given state steps to. Typically this means that the semantics has gotten stuck, but in this case there is another possibility: the control in question is not part of the core language, and should be handled by the extension system. A simple example of a non-core instruction would be

CHAPTER 6. ENGINEERING ISOLATION

 a trap to the operating system; in Concurrent C minor the extension instructions are the concurrent instructions make lock, free lock, lock, unlock, and fork.

6.3.1 Axioms and basic definitions The EXTENSIBLE SEMANTICS module type also contains certain axioms and basic definitions about the step relation that must be satisfied;

these are largely given in figure 6.5. Axioms are part of the module type to isolate and centralize the dependencies between the core and extension8.

The axiom step obeys rmap on lines 96–102 expresses the major reason to include resource maps (or footprints) in the semantics. The key is on lines 100–101: for each address, either the address is writable (i.e., VAL fullshare) or the value in memory before and after steping are equal9.

The axiom step preserves resource on lines 104–121 details how the step relation is allowed to change the resource map. In fact, very little is allowed to change. If the value was empty before stepping, then it must be empty afterwards (line 117). If not, then there are two possibilities; by far the most common is that if the value was a YES value, then it is preserved with the same kind, share, and predicate list While it has been shown in Coq that C minor satisfies all of the axioms presented; it has not yet been shown that these are all of the axioms required by the concurrency proofs, since the process of rebuilding the proof using this cleaner design is ongoing.

In the existance of byte-addressed memory, this property is more complicated.

6.3. AN EXTENSIBLE SEMANTICS  93 (* Axioms about the step relation *) 95 (* Memory does not change except for fully-owned data *) 96 Axiom step_obeys_rmap: forall ge st st’, 97 step ge st st’ match (from_state st, from_state st’) with 99 ((rmap, m, _),(_, m’, _)) = 100 forall addr, (writable (rmap @ addr)) \/ 101 (m addr = m’ addr) 102 end.

104 (* Required for CompCert memory model *) 105 Definition rmap_memory_model_rmap_ok (phi phi’: rmap) := 106-111 (* See figure 5.8 *) 113 Axiom step_preserves_resource: forall ge st st’, 114 step ge st st’ match (from_state st, from_state st’) with 116 ((rmap, _, _),(rmap’, _, _)) = forall addr, 117 (rmap @ addr = NO rmap - rmap’ @ addr = NO rmap’) /\ 118 ((forall sh k LP, rmap @ addr = YES rmap k sh LP rmap’ @ addr = YES rmap’ k sh LP) \/ 120 (rmap_memory_model_rmap_ok rmap rmap’)) 121 end.

123 (* Determinism *) 124 Axiom step_fun: forall ge st st1 st2, 125 step ge st st1 - step ge st st2 - st1 = st2.

127 (* Required for model of resource maps *) 128 Axiom step_not_any_younger:



Pages:     | 1 |   ...   | 8 | 9 || 11 | 12 |   ...   | 22 |


Similar works:

«SHOPLIFTING AS CONSUMER MISBEHAVIOUR An exploratory study of shoplifting applying a consumer behaviour approach Thesis submitted for the degree of Doctor of Philosophy at the University of Leicester by Michele Tonglet B.A. (Hons), Dip M. University College Northampton April 1999 UMI Number: U594549 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...»

«SEEKING SALVATION: BLACK MESSIANISM, RACIAL FORMATION, AND CHRISTIAN THOUGHT IN LATE TWENTIETH CENTURY BLACK CULTURAL TEXTS by Deidre Lyniece Wheaton A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (American Culture) in The University of Michigan Doctoral Committee: Associate Professor Angela D. Dillard, Co-Chair Associate Professor Joshua L. Miller, Co-Chair Associate Professor Tiya Miles Professor Ifeoma Nwankwo, Vanderbilt University...»

«UNIVERSITY OF CALIFORNIA, IRVINE Enhancing Architecture-Implementation Conformance with Change Management and Support for Behavioral Mapping DISSERTATION submitted in partial satisfaction of the requirements for the degree of DOCTOR OF PHILOSOPHY in Information and Computer Science by Yongjie Zheng Dissertation Committee: Professor Richard N. Taylor, Chair Professor André van der Hoek Assistant Professor James A. Jones © 2012 Yongjie Zheng DEDICATION To Mom and Dad. ii TABLE OF CONTENTS Page...»

«DO NORMATIVE JUDGEMENTS AIM TO REPRESENT THE WORLD? Bart Streumer b.streumer@rug.nl Ratio 26 (2013): 450-470 Also in Bart Streumer (ed.), Irrealism in Ethics Published version available here: http://dx.doi.org/10.1111/rati.12035 Abstract: Many philosophers think that normative judgements do not aim to represent the world. In this paper, I argue that this view is incompatible with the thought that when two people make conflicting normative judgements, at most one of these judgements is correct....»

«Université de Montréal Influence du milieu d'évaluation sur la réalisation de tâches liées à la préparation de repas auprès de personnes âgées fragiles par Véronique Provencher École de réadaptation Faculté de médecine Thèse présentée à la Faculté des études supérieures en vue de l’obtention du grade de Philosophiæ Doctor (Ph.D.) en sciences biomédicales option réadaptation Juin, 2012 ©Véronique Provencher, 2012 Université de Montréal Faculté des études...»

«EFFECTS OF CHRONIC METHYLMERCURY EXPOSURE ON REPRODUCTIVE SUCCESS, BEHAVIOR, AND STEROID HORMONES OF THE WHITE IBIS (Eudocimus albus) By NILMINI JAYASENA 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 2010 1 © 2010 Nilmini Jayasena 2 To my parents 3 ACKNOWLEDGMENTS First and foremost, I wish to extend my sincere gratitude to my major adviser, Dr. Peter Frederick...»

«IRON FILE SYSTEMS by Vijayan Prabhakaran B.E. Computer Sciences (Regional Engineering College, Trichy, India) 2000 M.S. Computer Sciences (University of Wisconsin-Madison) 2003 A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Computer Sciences University of Wisconsin-Madison Committee in charge: Andrea C. Arpaci-Dusseau (Co-chair) Remzi H. Arpaci-Dusseau (Co-chair) David J. DeWitt Mary K. Vernon Mikko H. Lipasti ii iv v Abstract IRON...»

«A METHOD FOR THE DEVELOPMENT OF AN EFFECTIVE FLOW DIVERTING DEVICE FOR TREATMENT OF CEREBRAL ANEURYSMS A DISSERTATION SUBMITTED TO THE FACULTY OF THE GRADUATE SCHOOL OF THE UNIVERSITY OF MINNESOTA BY Ricky Chow IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Eph Sparrow, PhD September 2013 ACKNOWLEDGEMENTS The author is extremely grateful for the following people who have provided emotional guidance, financial support, experimental resources, learning...»

«DIELECTRIC PHENOMENA OF OXIDES WITH FLUORITE RELATED SUPER STRUCTURES By CHRISTOPHER GEORGE TURNER 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 © 2014 Christopher Turner To my parents, friends and everyone who helped me push through the last four years ACKNOWLEDGMENTS First, I would like to thank my advisor Dr. Juan C. Nino for his support and guidance. He...»

«IMPACT OF MARKET DEMAND AND GAME SUPPORT PROGRAMS ON CONSUMPTION LEVELS OF PROFESSIONAL TEAM SPORT SPECTATORS AS MEDIATED BY PERCEIVED VALUE By KUN-WUNG BYON 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 © Kun-wung Byon To my family ACKNOWLEDGMENTS I would like to show my deepest appreciation to my advisor, Dr. James J. Zhang for his endless support throughout...»

«Global Co-Operation in the New Millennium The 9th European Conference on Information Systems Bled, Slovenia, June 27-29, 2001 GENDER, EMANCIPATION AND CRITICAL INFORMATION SYSTEMS Alison Adam Information Systems Research Centre, University of Salford, Salford M5 4WT, UK Tel: +44 (0)161 295 3125 Fax: +44 (0)161295 5559 a.adam@salford.ac.uk Alison Adam ABSTRACT This paper addresses ways in which theorizing gender may be important in forming an understanding of the topic of emancipation which is...»

«SERVICE-ORIENTED ARCHITECTURE FOR INTEGRATION OF BIOINFORMATIC DATA AND APPLICATIONS A Dissertation Submitted to the Graduate School of the University of Notre Dame in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy by Xiaorong Xiang, B.S., M.S. Gregory R. Madey, Director Graduate Program in Computer Science and Engineering Notre Dame, Indiana April 2007 c Copyright by Xiaorong Xiang All Rights Reserved SERVICE-ORIENTED ARCHITECTURE FOR INTEGRATION OF...»





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