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



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

«A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in Electrical Engineering and Computer ...»

-- [ Page 11 ] --

The word asynchronous is derived from the Greek word ασύγχρονος. The latter is a compound of the privative prefix α-, the prefix συν-, in the sense of of identical, and χρόνος, the Greek word for time. It is used in a strict sense to assert that one does not coincide in time with another, or, more often, in a loose sense to assert that one need not coincide in time with another. And in the context of concurrency theory, it is the only in a loose sense that it can be used without any contradiction. For if two events must be non-synchronized, then there is a synchronization between the presence of the one and absence of the other.

CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 94

The most important implication from this intuitive notion of asynchrony is that communication must be unidirectional. In other words, in an asynchronous setting, if a process wants to communicate with another process, then the most it can do is pass a message for it to read at its own leisure. And this means that there must be some place to leave that message. Therefore, a process is determined by a number of ports, or mailboxes, as we like to call them, which is the interface of the process to the outside world.

Based on this, we shall now give an informal, anthropomorphic description of how we think an asynchronous process works. The precise concept will only be understood after the axioms are presented. But this informal description will be very useful in understanding the intuition behind the mathematics, and we shall return frequently to it. We only advise the reader not to take it too literally.

We shall then think of an asynchronous process as an organization of people. And this organization will communicate with the outside world through the exchange of messages.

Specifically, it will have a number of mailboxes, and a number of workers and messengers.

We will not constrain the internal structure of the mailboxes at all. These may act as bounded or unbounded buffers, first-in-first-out queues or push-and-pop stacks, single-token places or multisets. The workers inside the organization will be responsible for the operation of the organization, and their access to these mailboxes will too be left unconstrained. For all we know, a worker might choose to ignore all messages, or might be sitting behind a mailbox waiting for the next message. Finally, the messengers will be responsible for delivering messages to other organizations, and thus, represent the communication capabilities of the organization. And while the number of mailboxes will be considered fixed for an organization, the number of workers and messengers will, in principle, be allowed to vary.

Here, we will focus on a specific type of asynchronous process, a sequential asynchronous process. What this corresponds to in our anthropomorphic description is the constraint that there be just one worker. Messengers may by many and variable, but there is always going to be a single worker.

4.2 Asynchronous process types Our first step is to formalize this anthropomorphic notion of interface of a process.

Definition 4.2.1. An asynchronous process type is an ordered pair I, O such that the

following are true:

–  –  –

(c) dom I and dom O are disjoint.

In an asynchronous process type I, O, I represents that mailboxes of a process, and the types of messages that can be deposited to them. O, on the other hand, represents all the mailboxes that a process might deposit a message to, and all the kinds of messages it might deposit. This creates some redundancy, but a typed approach greatly simplifies things.

Note that the constraint that dom I and dom O be disjoint makes sense from an observational point of view: if a process deposits a message to itself, only it can observe that deposition.

One interesting question here is why we have decided to make the number of input and output channels countable when we have intentionally left everything else unbounded. The reason is simple: our executions are finite or infinite sequences, as they must be if we want our processes to maintain a connection with reality. And thus, a process with an uncountable number of channels could never communicate over all of them through its lifetime.

4.3 Systems and coalgebras The type of an asynchronous process determines the different kinds of actions that it can perform. Basically, these are input actions, which are to be understood as the event of deposition of a message to a mailbox of the process, output actions, which correspond to the deposition of a message by a messenger of the process to some mailbox, and internal actions, which model the work done internally by the workers of the process.

Assume an asynchronous process type I, O.

We write actin I, O for { i, m | i ∈ dom I and m ∈ I(i)}.

We write actout I, O for { o, m | o ∈ dom O and m ∈ O(o)}.

We write τ for ∅.

We write act I, O for actin I, O ∪ actout I, O ∪ {τ }.

CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 96

We call any i, m ∈ actin I, O an input action, any o, m ∈ actout I, O an output action, and τ an internal action.

Notice that the choice of ∅ for τ is arbitrary. Any object different from an ordered pair would do. The symbol itself is used for conformance with the literature.





It is also worth noting that there is no predefined set of actions. Any pair of functions satisfying the definition of an asynchronous process type will do.

We now begin to formalize our notion of process. The first step is to define a notion of path. This is understood as any finite or infinite sequence of steps through the underlying transition system of a labelled execution system.

Assume an (act I, O )-labelled execution system S, E.

We write paths S, E for the largest subset X of S × S (act I, O × S) such that for every

s, e ∈ X, one of the following is true:

(i) e = ;

α (ii) there is α, s, and e such that s −→trans E s, s, e ∈ X, and ·e.

e= α, s The existence of a largest such set is easily verified by straightforward order-theoretic arguments, which we will henceforth omit.

We next begin to define a notion of fairness for such paths. Intuitively, we want every different party involved in the execution of a process to be given the chance to proceed.

This include the worker of the process, the messengers, and of course the environment.

However, we want to place as little constraints as possible, making sure that in the end, every possible interleaving of them will be part of the behaviour of the process.

Assume s, e ∈ paths S, E.

We say that τ is eventually in s, e if and only if s, e is a member of the smallest set X

such that the following are true:

τ (i) for every s, s, and e, if s −→trans E s and s, e ∈ paths S, E, then s, τ, s · e ∈ X;

α (ii) for every s, α, s, and e, if s −→trans E s and s, e ∈ X, then s, α, s · e ∈ X.

–  –  –

The meaning of these two predicates should be clear. The first asserts that in an execution, the worker does at some point make progress, and the second that at some point in the execution, the worker cannot make progress.

The following is meant to take care the progress of a messenger.

o,m Assume o, m ∈ actout I, O and s such that s −→ trans E s.

We say that o, m, s is eventually in s, e if and only if s, e is a member of the

smallest set X such that the following are true:

–  –  –

Here, the situation is more complex. The problem is that at any point, there may be more than one messenger with identical messages and destinations. If we used the same type of predicate as in the case of an internal action, there would be cases where a messenger was put on hold forever, just because another messenger with the same message and destination was making progress. And for all we know, the behaviour of the worker may depend on the identity of the available messengers. In Definition 4.3.1, the necessary confluence constraints are imposed so that the above method does indeed guarantee that every single messenger will eventually make progress.

With these inductively defined predicates, we can now define a notion of fairness coinductively.

We say that s, e is fair in S, E if and only if s, e is a member of the largest subset X

of paths S, E such that for every s, e ∈ X, one of the following is true:

–  –  –

We note that similar approaches of iterated induction and coinduction to fairness have been used before (for example, see [45]).

By requiring the executions of a process to coincide with all fair paths in the underlying labelled transition system, we guarantee that all different interleavings of the worker, the messengers, and the environment are accounted for.

Definition 4.3.1.

A sequential asynchronous process system of type I, O is an (act I, O )-labelled execution system S, E such that the following are true:

–  –  –

We briefly go over the clauses of this definition.

Clause (a) corresponds to the most basic assumption of asynchrony, that we should be able to deposit any kind of message in any mailbox at any time. Diagrammatically, we have the

following representation:

–  –  –

Here, the dashed line is used to signify existence of the corresponding transition, which is understood as a transition of the underlying labelled transition system of the sequential asynchronous process system.

Clause (b) formalizes the idea that the effect of deposition of a message in a mailbox is uniquely determined. In other words, there are no different ways of depositing a message in

a mailbox. Diagrammatically, we have the following:

CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 100

–  –  –

Clause (c) is the last clause concerned with input, and what it states is essentially that different mailboxes are physically distinct. Thus, depositing messages to two different mailboxes in any order will have the same effect in the content of each mailbox. This is

portrayed in the following confluent diagram:

–  –  –

Clauses (d), (e), and (f) are concerned with output, and essentially, assert that a messenger can never be recalled. Once a decision is made, and a messenger is dispatched, that messenger will insist until his job is done. This is expressed by the confluence of the

following three diagrams:

–  –  –

Clause (g) is the last of the clauses that constrain the underlying labelled transition system, and is, as we shall see, somewhat controversial. Essentially, what it asserts is that it cannot be the case that a worker waits for a messenger to continue with his job. This clearly precludes the situation where there is only one person in the organization, switching between a worker and a messenger. This is the intuitive idea behind the following

commutative diagram:

CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 101

–  –  –

Finally, clause (h) is the place where our work begins to pay off. All previous clauses concern transitions, and while more general than the typical approach to asynchrony (for example, see [59]), are after all expressed in terms of labelled transition systems. It is in (h), where we begin to express properties about our systems that are impossible to capture with labelled transition systems. And this will become all the more important, when we use our coalgebraic framework to obtain an extensional model for these properties.

To be formal, we repeat all the above, this time for labelled execution coalgebras.

Assume an (act I, O )-labelled execution coalgebra C, ε.

We write paths C, ε for the largest subclass X of C × Seq(act I, O × C) such that for

every c, e ∈ X, one of the following is true:

–  –  –

Assume c, e ∈ paths C, ε.

We say that τ is eventually in c, e if and only if c, e is a member of the smallest set X

such that the following are true:

–  –  –

We say that c, e is fair in C, ε if and only if c, e is a member of the largest subset X

of paths C, ε such that for every c, e ∈ X, one of the following is true:

–  –  –

Definition 4.3.2.

A sequential asynchronous process coalgebra of type I, O is an (act I, O )-labelled execution coalgebra C, ε such that the following are true:

–  –  –

Clearly, sequential asynchronous process systems and small sequential asynchronous process coalgebras are the same objects in different guises.

Assume a sequential asynchronous process system S, E of type I, O.

CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 104

Assume a sequential asynchronous process coalgebra C, ε of type I, O.

The following is immediate from :

Proposition 4.3.3. The following are true:

(a) the (act I, O )-labelled execution coalgebra S, fun E is a sequential asynchronous process coalgebra of type I, O ;

(b) if C, ε is small, then the (act I, O )-labelled execution system C, rel ε is a sequential asynchronous process system of type I, O.

We write SAPC I,O for the category whose objects are all the asynchronous process coalgebras of type I, O, and arrows all the homomorphisms from one asynchronous process coalgebra of type I, O to another.

Clearly, SAPC I,O is a full subcategory of (Pow ◦ Seq ◦ (act I, O × Id))-Coalg.

The following is straightforward from Proposition 3.3.1 and a routine proof by cases:

Theorem 4.3.

4. SAPC I,O is a (Pow ◦ Seq ◦ (act I, O × Id))-covariety.



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


Similar works:

«Creating and Sharing Structured Semantic Web Contents through the Social Web Aman SHAKYA DOCTOR OF PHILOSOPHY Department of Informatics, School of Multidisciplinary Sciences, The Graduate University for Advanced Studies (SOKENDAI) 2009 (School Year) September 2009 A dissertation submitted to The Department of Informatics, School of Multidisciplinary Sciences, The Graduate University for Advanced Studies (SOKENDAI) In partial fulfillment of the requirements for The degree of Doctor of Philosophy...»

«Creating Green Chemistry: Discursive Strategies of a Scientific Movement Jody A. Roberts Dissertation submitted to the Faculty of Virginia Polytechnic Institute and State University in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Science and Technology Studies Committee: Richard M. Burian (chair) Daniel Breslau Richard F. Hirsh Timothy W. Luke Joseph C. Pitt 13 December 2005 Keywords: Green Chemistry, Scientific Movements, Chemistry Studies, Discursive...»

«Treatment of trochanteric and subtrochanteric hip fractures Sliding hip screw or intramedullary nail? Dissertation for the degree of philosophiae doctor (PhD) at the University of Bergen Scientific environment “The Intertan Study” (papers I and IV) was performed at the Orthopaedic Department, Haukeland University Hospital (HUS), and in close teamwork with the Clinical Research Unit and the Department of Radiology at HUS. “The Intertan Study” was also based on a close collaboration with...»

«Black Males' Perceptions of and Experiences with the Police in Toronto by Akwasi Owusu-Bempah A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Centre for Criminology and Sociolegal Studies University of Toronto © Copyright by Akwasi Owusu-Bempah, 2014 Black Males' Perceptions of and Experiences with the Police in Toronto Akwasi Owusu-Bempah Doctor of Philosophy Centre for Criminology and Sociolegal Studies University of Toronto Abstract Canada is...»

«Observing and influencing preferences in real time Gaze, morality and dynamic decision-making Philip Pärnamets DOCTORAL DISSERTATION by due permission of the Faculty of Humanities, Lund University, Sweden. To be defended at LUX, room C121, Lund, April 18, 2015, at 13:15. Faculty opponent Alan Kingstone Lund University Cognitive Science Document name Department of Philosophy Doctoral dissertation LUND UNIVERSITY Date of issue 2015-04-18 Author(s) Philip Pärnamets Sponsoring organization Title...»

«COMBINED EXPERIMENTAL/THEORETICAL APPROACH TOWARD THE DEVELOPMENT OF CARBON TOLERANT ELECTROCATALYSTS FOR SOLID OXIDE FUEL CELL ANODES by Eranda Nikolla 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: Assistant Professor Suljo Linic, Co-chair Professor Johannes W. Schwank, Co-chair Professor Erdogan Gulari Professor John W. Halloran Professor Phillip E. Savage ©...»

«Universidade Federal de Goiás Faculdade de Ciências Humanas e Filosofia Programa de Pós-Graduação em Sociologia Mestrado em Sociologia Identidade e Territorialidade entre os Kalunga do Vão do Moleque Thais Alves Marinho Goiânia, Março de 2008. Universidade Federal de Goiás Faculdade de Ciências Humanas e Filosofia Programa de Pós-Graduação em Sociologia Identidade e Territorialidade entre os Kalunga do Vão do Moleque Dissertação apresentada ao Programa de PósGraduação em...»

«co-construction of hybrid spaces Åsa Rudström A Dissertation submitted to the University of Stockholm in partial fulfilment of the requirements for the Degree of Doctor of Philosophy Department of Computer and Systems Sciences Stockholm University and Royal Institute of Technology November 2005 Department of Computer and Systems Sciences Swedish Institute of Computer Science Stockholm University and Royal Inst. of Technology P.O. Box 1263 Forum 100 S164 29 Kista S164 40 Kista SWEDEN SWEDEN...»

«December 2015 JEANNE CAMPBELL REESMAN Department of English University of Texas at San Antonio 7731 Broadway, #C-314 One UTSA Circle San Antonio, TX 78209 San Antonio, TX 78249 (210) 826-8613 (h) ph. (210) 458-5133; fax (210) 458-5366 (210) 867-9718 (c) http://colfa.utsa.edu/English/reesman.html jeanne.reesman@utsa.edu Administrative Positions Graduate Advisor of Record, Ph.D. Program in English University of Texas at San Antonio, 2010-2014 Interim Dean of Graduate Studies University of Texas...»

«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? This sounds like the set-up for a bad joke. The term suburbia often conjures up caricatured images of plastic, white, middle-class Americans driving gas-guzzling Suburban Utility Vehicles past white picket...»

«ESSAYS ON MERGERS & ACQUISITIONS AND INNOVATION by Yu Yu This thesis/dissertation document has been electronically approved by the following individuals: Rao,Vithala R. (Chairperson) Kadiyali,Vrinda (Minor Member) Nicholson,Sean (Minor Member) ESSAYS ON MERGERS & ACQUISITIONS AND INNOVATION A Dissertation Presented to the Faculty of the Graduate School of Cornell University In Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy by Yu Yu August 2010 © 2010 Yu Yu...»

«Hideaki Shimazaki, Ph.D RIKEN Brain Science Institute 2-1 Hirosawa, Wako, Saitama 351-0198 Japan Phone: +81-48-467-9644 Fax: +81-48-467-9670 E-Mail: shimazaki@brain.riken.jp HP: http://goo.gl/viSNG Education Doctor of Philosophy, Kyoto University 2004 Apr 2007 Mar Department of Physics, Graduate School of Science, Kyoto University, Kyoto, Japan. Supervisor: Prof. Shigeru Shinomoto Thesis title: Recipes for selecting the bin size of a histogram. Master of Arts (Neuroscience), Johns Hopkins...»





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