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



Pages:     | 1 |   ...   | 14 | 15 || 17 | 18 |   ...   | 22 |

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

-- [ Page 16 ] --

Recall from section 6.6 that to extend a core semantics one defines an oracle type and then constructs a consult relation consult : program × oracle × state → option(oracle × state), which implements the extended statements. Recall that a state σ is a pair of a world w and a control κ. A world is a level-independent tuple of locals ρ, resource map φ, and memory m; it also contains a map from global names to addresses, but this has been elided from the presentation. A control contains the level-specific portions of the state, primarily program syntax.

For the sequential submachine, the oracle type will be unit because the make lock and free lock statements do not need any auxilary state.

Nontrivial oracles are needed only for interpreting the meaning of the fully-concurrent instructions lock, unlock, and fork, which the sequential submachine does not attempt to implement.

 CHAPTER 8. CONCURRENT OPERATIONAL SEMANTICS

–  –  –

Figure 8.2: The consult relation of the sequential submachine We define consult in figure 8.

2. To execute make lock v R, the machine ensures that the location is fully-owned data containing a zero, and updates the resource map to treat the location as a lock with invariant R. The lock is created with 100% visibility and is also created held. Since a lock at location l is “locked” if memory at l is zero, the lock is created locked, and the make lock statement only changes the resource map. We use the exactly predicate to make sure that the world does not change in any other way.

To execute free lock v, the machine reverses make lock. First it verifies that the lock is entirely owned and held, and then updates the resource map to show that the location is fully-owned data containing a zero. Since the lock is held, the memory will contain a zero at v.

–  –  –

completes the execution of an extended statement or gets stuck.

Using the definitions given in section 6.6 we can build a step ress lation −→ for the sequential submachine using the core step relation −→ defined in figure 8.1 and the consult relation defined in figure 8.2.

This step relation will be a conservative approximation to the erased e sequential step relation −→.

–  –  –

case, Oracle Step, means that our consult has succeeded, in which case there are two subcases: one for make lock and one for free lock. In both cases we do not change ρ or m and transition to control κ. This is exactly what is done for these statements in the erased sequential step given in figure

5.1. The third case, Oracle Diverges, is impossible because our consult relation never returns None.

–  –  –

where ℧ is a schedule, θ is a thread list, L is a lock pool, φmp is a memory pool, φfp is a function pool, and m is a memory. The memory is exactly the same as in the sequential semantics. Each of the other components will be explained in sections 8.3.1–8.3.4 below. A concurrent machine state also comes with a set of consistency requirements, as explained in section 8.4. For this presentation, any concurrent machine state should be considered consistent.

8.3.1 Schedule A schedule ℧ is a finite list of natural numbers, which act as threadIDs. The number at the head of the schedule tells the concurrent operational semantics which thread to execute next. When the schedule runs out, the concurrent machine safely halts computation. Our reason for quantifing over finite schedules was explained in section 5.2.

8.3.2 Threads The purpose of a concurrent machine is to execute multiple threads of

–  –  –

source map φ; in contrast, m is not part of a thread because all threads must use the same memory.

8.3.3 Lock pool A lock pool L is a partial function from the addresses of unlocked locks to resource maps. In our setting, every resource must be owned by somebody at all times. Normally, resources are owned by the threads.

However, when a lock is unlocked, a thread gives up the resources (i.e., the resource map) associated with the lock. When a thread is unlocking a lock we do not wish to make the thread wait for the next thread to lock the lock. Therefore, we need a place to hold the resource map associated with the lock; this place is the lock pool L. When the next thread grabs the lock, we transfer the resources from the lock pool to the next thread.

The look pool not simply a resource map. Instead, it is a partial function from addresses to resource maps because this structure greatly simplifies the proof by making it trivial to show that all the resource maps associated with unlocked locks are disjoint.

8.3.4 Alloc and function pools The alloc pool φmp and function pool φfp are resource maps that own of two kinds of global resources. Each thread is given access to these global resources as it executes and relinquishes them when it yields to the next thread.

 CHAPTER 8. CONCURRENT OPERATIONAL SEMANTICS

The alloc pool is the owner of the unallocated but allocatable memory, and is used to allocate activation records on the stack at function call. In the CompCert memory model there is an unlimited amount of memory available for the stack3.





The function pool is the owner of all of the functions. In other words,

–  –  –

and all of the other resource maps in the system lack functions. The function pool allows all of the threads to have access to all of the functions. Passing the function pool around from thread to thread is not particularly beautiful, but it does ensure that the functions are available for all threads in a standard way. Developing an elegant way to guarantee global function availablity is suprisingly difficult, and thus is left for future work.

8.4 Consistent machines A concurrent machine state carries with it a set of consistency properties that ensure that it is well-formed. In Coq we ensure the consistency In a sequential program the alloc pool is a reasonable abstraction, as the operating system will terminate any program whose stack space grows beyond the available memory in the machine, and the CompCert compiler only makes partial correctness guarantees. In a concurrent program the situation is more complicated, since additional checks must be inserted in the function call to make sure that the thread is not about to exceed its stack space. In a high-level language like Concurrent C minor, checks are inserted by the compiler when it compiles a function call into lower-level languages; however this abstraction may not allow us to adapt our concurrency system for lower compiler levels, an open problem for future work.

8.4. CONSISTENT MACHINES  of concurrent machine states with a dependently-typed record.

8.4.1 Existence of total resource map The first property is the existence of a total resource map φT that is the join of all of the resource maps in the threads θ, all the resource

maps in the lock pool L, the alloc pool φmp, and the function pool φfp :

–  –  –

In other words, the individual resource maps combine into a cohesive whole φT. This guarantees, for example, that two distinct threads cannot have full ownership of a location at the same time. Thus, if a thread can write to a memory location, then no other thread can read from it.

The remaining properties all use φT.

8.4.2 Sufficient schedule

–  –  –

We will be trivially safe if we reach approximation level 0.

 CHAPTER 8. CONCURRENT OPERATIONAL SEMANTICS

8.4.3 Only waiting on locks The third property is that if a thread’s concurrent control is Klock v κ, then v is a lock in φT.

We use a function from resources to resource kinds:

–  –  –

We use rkind instead of the YES pseudoconstructor because it lets us ignore the pre- and postconditions of the function and so provide a cleaner characterization. The advantage here is relatively minor, but as explained in section 8.4.6, rkind also interacts better with age in the presence of implication, and there it is vital.

Using rkind it is easy to define the property that threads can only

wait on locks, as opposed to, e.g., regular data:

–  –  –

8.4.4 Well-formed alloc pool The fourth property is that the alloc pool φmp is well-formed. We enforce well-formedness by defining a predicate allocpool, which abstracts the nature of the CompCert memory model, and express the property as

–  –  –

where we use the memory m in the concurrent machine state.

8.4.5 Well-formed function pool

The fifth property is that the function pool φfp contains all of the functions. First we split off the φfp from φT, as follows:

–  –  –

The resource mape φnf is everything in φT that is not a function.

Using rkind it is straightforward to express property P1, that φnf

does not contain any functions:

–  –  –

The fifth property is just the conjunction of P1 and P2.

8.4.6 Well-formed lock pool The sixth property is a series of requirements on the lock pool. This turns out to be a bit trickier to define than expected. The most critical property is that we would like something like the following, which we

call P1(φT, L):

–  –  –

In other words, for every lock in the total resource map φT, if that lock is unlocked (i.e., if the memory at the lock location contains the value lock unlocked, which is 1), then the lock invariant holds on the associated resource map in the lock pool L.

The problem is that we need this property to be true even if the

–  –  –

Unfortunately, as P1 is stated, this is simply not true.

The first problem is the existence of wild terms in the model. If w |= R, it is not necessarily the case that w ′ |= R for some more approximate w ′. In chapter 7 we introduced the concept “necessary” to handle this issue. In chapter 4 we introduced the tightly operator, and said that the precondition for unlocking a lock with invariant R was tightly R. In section 7.3.8, we show that tightly is defined with the operator, and show that therefore tightly R is necessary. Therefore we

attempt to fix the problem with property P2(φT, L):

–  –  –

Unfortunately, there is still a problem with this definition that prevents it from ageing gracefully.

Recall from section 7.3.7 that because implication is contravariant in its antecedent, it does not play nicely with approximation. Unfor CHAPTER 8. CONCURRENT OPERATIONAL SEMANTICS tunately P1 and P2 use the YES pseudoconstructor in an antecedent, which in turn uses stratify, which approximates R. The solution is to use rkind in the antecedent, since it does not require R, and to quantify over the resource invariant existentially instead of universally, leading

to property P3(φT, L):

–  –  –

P3 does behave gracefully under ageing, and, informally, means almost the same thing as P1: In other words, for every lock in the total resource map φT, if that lock is unlocked (i.e., if the memory at the lock location contains the value lock unlocked, which is 1), then the lock invariant holds on associated resource map in the lock pool L.

In the actual Coq development, we use a weaker variant of P3, which we call P3′, and in which we only guarantee ⊲ tightly R instead

of tightly R:

–  –  –

antee than P3, meaning that it is easier to introduce but harder to use.

In future work we plan to move the Coq development from P3′ to P3.

In addition to P3′, we require that for each lock location l, memory at l is either lock unlocked (1) or lock locked (0); we also require that if a lock is locked, then l not be in the domain of the partial function L.

8.5 Concurrent step relation The full concurrent small-step relation is given in figures 8.3 and 8.4.

Figure 8.3 contains the portion of the step relation that is responsible for executing sequential statements.

The key sequential rule is cstep-seq, which uses the core semantics of the sequential submachine to perform a sequential step (recall from section 6.6 how we construct the −→ relation from consult). The head of the schedule is i, meaning that the next thread to execute is θi, which is equal to (ρ, φ, Krun κ).

First the alloc and function pools are joined to φ to make φs, and then we build a world (ρ, φs, m) and step in the sequential submachine with that world and the control κ to a subsequent world (ρ′, φ′s, m′ ) and control κ′. Since the sequential submachine’s oracle has type unit we use the value tt as a parameter to the step relation.

After taking a step in the submachine, we split out new alloc and function pools from φ′s. The submachine is allowed to age the resource

 CHAPTER 8. CONCURRENT OPERATIONAL SEMANTICS

–  –  –

Figure 8.3: Sequential steps in the concurrent step relation map to make it more approximate if it wishes, and so we allow the function pool, lock pool, and other threads to age as well so that all resource maps will have the same level and therefore will be able to join together into a total resource map.

One key point is that the schedule does not change during cstepseq. Thus the next instruction to be executed will be from the same thread—that is, the concurrent step relation does not context switch when executing normal sequential instructions. In section 5.3 we disCONCURRENT STEP RELATION 

–  –  –

Figure 8.4: Fully concurrent steps in the concurrent step relation

 CHAPTER 8.

CONCURRENT OPERATIONAL SEMANTICS

cussed why this is reasonable.



Pages:     | 1 |   ...   | 14 | 15 || 17 | 18 |   ...   | 22 |


Similar works:

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

«Ivan Illich Kreftingstr. 16 D 28203 Bremen Philosophy. Artifacts. Friendship Printed: 05.10.01 Filename and date: Philarpu.doc STATUS: To be pusblished in: Ivan Illich, Mirror II (working title). Copyright Ivan Illich.For further information please contact: Silja Samerski Albrechtstr.19 D 28203 Bremen Tel: +49-(0)421-7947546 e-mail: piano@uni-bremen.de Ivan Illich: Philosophy. Artifacts. Friendship 1 Ivan Illich PHILOSOPHY. ARTIFACTS. FRIENDSHIP I speak as a xenocryst. Deus in adjutorium...»

«DETERMINATION OF FOLDING PATHWAY SELECTION AND ORIGINS OF COOPERATIVITY OF NATURALLY OCCURRING AND DESIGNED CONSENSUS LEUCINE-RICH REPEAT PROTEINS by Thuy Phuong Dao A dissertation submitted to Johns Hopkins University in conformity with the requirements for the degree of Doctor of Philosophy Baltimore, Maryland June 2014 © Thuy Phuong Dao 2014 All rights reserved Abstract Thermodynamic and kinetic studies of linear repeat proteins have provided unique insights into cooperativity, detailed...»

«Faculté de génie Département de génie civil BEHAVIOR OF CIRCULAR CONCRETE COLUMNS REINFORCED WITH FRP BARS AND STIRRUPS Comportement de colonnes circulaires en béton armé de barres et de cadres de PRF Thèse de doctorat Spécialité: génie civil Mohammad M. Zaki M. Afifi A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Civil Engineering) Jury: Prof. Brahim BENMOKRANE (directeur de recherche) Prof. Amir FAM Prof. Amr EL RAGABY...»

«Ghent University Faculty of Arts and Philosophy “I AM NOT SURE IF THIS IS A HAPPY ENDING” THE QUEST FOR FEMALE EMPOWERMENT IN ANGELA CARTER’S WISE CHILDREN Supervisor: Dissertation submitted in partial fulfilment of the requirements for the degree of “Master in Professor Marysa Demoor de Taalen Letterkunde: Engels” by Aline Lapeire 2009-2010 Lapeire ii Lapeire iii “I AM NOT SURE IF THIS IS A HAPPY ENDING” THE QUEST FOR FEMALE EMPOWERMENT IN ANGELA CARTER’S WISE CHILDREN The...»

«FLEXIBLE NEURAL IMPLANTS Thesis by Ray Kui-Jui Huang In Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy CALIFORNIA INSTITUTE OF TECHNOLOGY Pasadena, California (Defended June 25, 2010) ii © 2011 Ray Kui-Jui Huang All Rights Reserved iii To My Family and Friends iv ACKNOWLEDGEMENTS This dissertation not only reflects the countless hours spinning photoresist, cleaning parylene machines, and mixing epoxy in Caltech Micromachining Laboratory, but it is also a...»

«A BEAM STEERING, BROADBAND MICROSTRIP ANTENNA FOR NON-CONTACT VITAL SIGN RADAR DETECTION By ZIVIN PARK 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 2011 1 © 2011 Zivin Park 2 To my father, mother, and grandmother, for their support and encouragement 3 ACKNOWLEDGMENTS I would like to express my sincere gratitude to my advisor Dr. Jenshan Lin for his advice,...»

«University of Connecticut DigitalCommons@UConn Articles Philosophy Department 7-1-2000 Physicalism and the Fallacy of Composition Crawford Elder University of Connecticut Department of Philosophy, crawford.elder@uconn.edu Follow this and additional works at: http://digitalcommons.uconn.edu/philo_articles Recommended Citation Elder, Crawford, Physicalism and the Fallacy of Composition (2000). Articles. Paper 3. http://digitalcommons.uconn.edu/philo_articles/3 This Article is brought to you for...»

«DEEP IN THE BURBS by STEVE THOMASON A Thesis Proposal Submitted to the Faculty of Luther Seminary In Partial Fulfillment of The Requirements for the Degree of DOCTOR OF PHILOSOPHY ST. PAUL, MINNESOTA SECTION ONE RESEARCH QUESTION The Question What do suburbia and spirituality have in common? The term suburbia often conjures up caricatured images of plastic, white, middle-class Americans driving gasguzzling Sport Utility Vehicles past white picket fences into cavernous garages that swallow them...»

«UNIDIMENSIONAL INTERPRETATION OF MULTIDIMENSIONAL TESTS Dissertation zur Erlangung des Doktorgrades der Philosophischen Fakultät der Christian-Albrechts-Universität zu Kiel vorgelegt von Steffen Brandt Kiel September 2015 Erstgutachter: Prof. Dr. Gabriel Nagy Zweitgutachter: Prof. Dr. Andreas Frey (Universität Jena) Tag der mündlichen Prüfung: 2. Februar 2016 Durch den zweiten Prodekan, Prof. Dr. John Peterson, zum Druck genehmigt: 3. Februar 2016 ZUSAMMENFASSUNG 3 Zusammenfassung...»

«Michigan Technological University Digital Commons @ Michigan Tech Dissertations, Master's Theses and Master's Reports Dissertations, Master's Theses and Master's Reports Open THE QUANTIFICATION OF THE FLY ASH ADSORPTION CAPACITY FOR THE PURPOSE OF CHARACTERIZATION AND USE IN CONCRETE Zeyad Tareq Ahmed Michigan Technological University Copyright 2012 Zeyad Tareq Ahmed Recommended Citation Ahmed, Zeyad Tareq, THE QUANTIFICATION OF THE FLY ASH ADSORPTION CAPACITY FOR THE PURPOSE OF...»

«Ryerson University Digital Commons @ Ryerson Theses and dissertations 1-1-2012 Sound as Signifier: Communication and Expression Through the Sound of Clothing Tala Kamea Berkes Ryerson University Follow this and additional works at: http://digitalcommons.ryerson.ca/dissertations Part of the Fashion Design Commons, and the Philosophy Commons Recommended Citation Berkes, Tala Kamea, Sound as Signifier: Communication and Expression Through the Sound of Clothing (2012). Theses and dissertations....»





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