Regions#

We discussed the syntax and semantics of regions.

Proposals for syntax included f @ r , by analogy to the location-assignment syntax Adrian was using for distributed Orc, or r { f }

r is a special region value, which governs some kind of region, like a simulation or a transaction.

Proposal for operational semantics included

        f -a-> f'
------------------------
R { f } -R(a)-> R { f' }

The region here is simply a transformer of events that occur during the evaluation of f. Note that this rule allows a region to affect how site calls return, since return events propagate upward from within f.

But this is not expressive enough. The region itself will almost certainly need to change state, which this rule does not allow.

 f -a-> f' R(a) = (R',a')
-------------------------------
 R { f } -a'-> R' { f' }

Now a region may change state each time an event occurs in f. This gives us more expressive power, especially if R is a partial function; if R is not defined for some transition that f would make, then that transition is not allowed while R remains the same.

However, this is still incomplete. How does a region halt? There is no elimination transition for regions.

Let's adopt the axiom: R { 0 } --tau--> 0

This makes the assumption that a region enclosing a finished execution is also finished. But this is not powerful enough: it does not allow the region to initiate computation on its own, for example to commit a completed transaction..

Here is a very powerful rule:

 f --a--> f' R(f',a) = (f'',a')
------------------------------------
 R { f } -a'-> f''

But this is probably too general; it is a summary of an entire class of possible operational semantics rules, and reasoning about the function R will be very difficult.

In conclusion, it is probably wiser to write operational rules for each kind of region separately; they may share some interesting common rules, but we can't write a single set of general rules to cover all possible regions of interest.

We are seeing, again and again, connections between regions and monads.

Real time and pruning#

We need a simple way to state the interaction between pruning and time.

Pruning is supposed to take the "first" value published by the right hand side; what rule determines which value is first?

Jay has suggested that the rule for pruning should be purely causal: if event X causes event Y, then when choosing between X and Y, X is always "first". If no causal relationship exists, then the choice is arbitrary.

It is obvious that if X causes Y, then X precedes Y in all traces. Thus, if pruning always takes some prefix of a trace, this causal rule can never be violated.

Normally the choice of "first" publication is arbitrary, since the Orc semantics alone can never create a causal relationship between two publication events. However, if events occur in the context of time, the timeline itself introduces additional causal relationships.

Jay reiterated David's earlier suggestion: real time is totally ordered. All events at time t cause all events at times t' where t < t'. Then, publications may be in a causal relationship because they occur at different times, and the causal definition of pruning makes sense.

Rethinking logical time#

We reached a new consensus on logical time: "local" sites take some amount of logical time (they may interact with other events in this timeline) "remote" sites take no logical time (they won't interact with other events in this timeline) This is almost exactly the reverse of our previous immediate/non-immediate conclusion.

We've returned to an old realization about logical time: a simulation can only make progress if all of the sites it calls also eventually return or halt. Previously we did not have the concept of "halt", so this was a difficult proposal, since not all sites could be guaranteed to return a value even under completely reasonable conditions; consider if(false). Now, this notion of coupled progress makes more sense. Some remaining problems:

What do we do about sibling timelines? What happens when two simulations with otherwise unrelated logical timers interact with a shared site, such as a channel?

What do we do about unbound variables? A simulation is still supposed to take zero logical time in the timeline of its parent. If the simulation has unbound variables when it starts, and those variables can only be bound in the parent by advancing its logical clock, then those variables are unbound "forever" in the context of the nested simulation, so we're stuck.

Adrian's example:

sim { x | LT(1) } <x< LT(2)
( sim { x } | LT(1) ) <x< LT(2)

Add new attachment

Only authorized users are allowed to upload new attachments.
« This page (revision-1) was last changed on 15-Dec-2010 16:48 by DavidKitchin