Lectures 9 and 10: 29th October 2019 Flashcards
Interleaving and communications
What is Eval(Var)?
Eval(Var) = the set of variable evaluations over Var that are possible = {η1, η3, ηn}
Var is a set of typed state variables
How are TSes defined?
Transition Systems are defined as (S, Act, T, I, AP, L)
where
S = finite set of states Act = finite set of actions: ~ inputs T = set of transitions, in form T ⊆ (S x Act x S): which state to go to from a current state for a given action I = set of initial states AP = set of atomic propositions L = labelling function: determines which APs hold in which states
How are PGs defiend?
A PG over set Var of typed variables is a tuple
PG = (Loc, Act, Effect, Ct, Loc0, g0) where
Loc is a set of locations
Act is a set of actions
Effect: Act × Eval(Var)→Eval(Var) is the effect function
Ct ⊆ Loc × Cond(Var) × Act × Loc is the conditional transition relation
Loc0 ⊆ Loc set of initial locations l1 –g:α–> l2
g0 ∈ Cond(Var) is the initial condition
every location in initial locations, Loc0, satisfies the initial condition, g0
Eval(Var) = η = set of variable evaluations over Var
Cond(Var) = set of boolean conditions over Var
Var is a set of typed state variables
What’s the difference between a TS and a PG?
PG has locations rather than states and its transitions are conditional, and effects of transitioning (=> action => changing Eval(Var)) are also defined. Interleaved PGs don’t interfere with global variables.
The program graph consisting of locations as nodes and conditional transitions as edges is not a transition system since the edges are provided with conditions.
However, each program graph can be interpreted as a transition system. The underlying transition system of a program graph results from unfolding: a state of the transition system is composed of a location l of the program graph and an evaluation η of the variables.
What is parallel composition?
( P || Q) expresses the parallel composition of the processes P and Q. It constructs an LTS which allows all the possible interleavings of the actions of the two processes. Actions, which occur in the alphabets of both P and Q, constrain the interleaving since these actions must be carried out by both of the processes at the same time. These shared actions synchronise the execution of the two processes. If the processes contain no shared actions then the composite state machine will describe all interleavings.
The parallel composition operator can be used to put processes in parallel. The behaviour of p ∥ q is the arbitrary interleaving of actions of the processes p and q, assuming for the moment that there is no communication between p and q. For example, the process a ∥ b behaves like a · b + b · a.
How does parallel composition work with TSes?
Doesn’t - may only be done with PGs
What is interleaving?
Composing combinations of actions by different program processes, examining only their effects on their local variables (doesn’t handle globals).
How does interleaving work with TSes?
The interleaving operator for transition systems simply
constructs the cartesian product of the individual state
spaces without considering potential conflicts from
shared variables.
Let TSi = (Si, Acti, Ti, Ii, APi, Li) be two interleaved transition systems.
TSi = TS1 ||| TS2 = (S1 × S2, Act1 ∪ Act2, T, I1 × I2, AP1 ∪ AP2, L)
where T is such that:
⟨s1, s2⟩ –α–> ⟨s’1, s2⟩
and
⟨s1, s2⟩ –β–> ⟨s1, s’2⟩
and L(⟨s1, s2⟩) = L1(s1) ∪ L2(s2) for α ∈ Act1, β ∈ Act2
What is the TS of a PG?
The TS(PG) of a PG = (Loc, Act, Effect, Ct, Loc0, g0) over Var is the tuple (S, Act, T, I, AP, L) where
????????
How does interleaving work with PGs?
The interleaving operator for transition systems simply
constructs the cartesian product of the individual state
spaces without considering potential conflicts from
shared variables. For programs with shared variables, we define interleaving directly on program graphs PG1 ||| PG2
Let PGi = (Loci, Acti, Effecti, C(t,i), Loc(0,i), g(0,i)) be two program graphs over variables
PGi = PG1 ||| PG2 over Var1 ∪ Var2 = (Loc1 × Loc2, Act1 ⊎ Act2, Effect, Ct, Loc(0,1) × Loc(0,2), g(0,1) ⋀ g(0,2))
⊎ = disjoint union ⋀ = conjuction (‘and’ operator)
⟨l1, l2⟩ –g:α–> ⟨l’1, l2⟩
and
⟨l1, l2⟩ –g:β–> ⟨l1, l’2⟩
and Effect(α, η)(v) = Effecti(α, η)(v) if α ∈ Acti, v ∈ Vari
When would you interleave PGs?
When interleaving programs with shared variables
What is an effect function?
Tells you what the outcome of each transition/action is on Eval(Var), i.e. how variable values change. The function takes start evaluation and action and gives outcome evaluation.
How do the possibility of transitions change after interleaving TSes? And PGs?
For both, any transitions that were possible in a component TS or PG prior to interleaving is still possible after interleaving without affecting other TSes/PGs.
How is interleaving different for PGs and TSes?
Interleaved PGs can’t interfere with global variables but this is possible in interleaved TSes.
Why can TS interleaving be described as the Cartesian product of states?
Interleaving TSes is just the Cartesian product of states to find all possible pairs.
How are the local (to each component PG) and global variables of a composed program graph defined?
- Local variables of PG1 are x1 ∈ Var1∖Var2
- Local variables of PG2 are those in x2 ∈ Var2∖Var1
- Global variables are x ∈ Var1 ∩ Var2
What are critical actions in composed PGs?
Actions that access global variables are critical. Critical actions cannot be executed simultaneously.
What are composed PGs?
A PG resulting from the parallel composition of two other PGs
What is the PG level? Why is it “higher”?
Modelling a program with a PG rather than a TS. It is a higher level because it doesn’t allow for global interference when interleaving and is another added conversion from a TS.
How is interleaving different from parallel composition?
Parallel composition is complete interleaving. It can only be done with PGs whereas incomplete interleaving can also be done with TSes. Complete interleaving doesn’t allow for processes (PGs) to interfere with global variables but incomplete interleaving does.
Why must composition with actions that affect global variables be carried out at the PG level?
PGs have an effect function that tells you the values of each variable after each action (transition), so in each state. They don’t interfere when being interleaved completely.
What is a semaphore?
A variable or abstract data type used to control access to a common resource by multiple processes in a concurrent system such as a multitasking operating system.
How can semaphores implement mutual exclusion?
Have a boolean of if in critical section or int above/below threshold value. Only allow in when false, set to true when in critical section or accessing a resource, then to false after to allow others in.
How do you interleave two PGs to enforce mutual exclusion?
Have 1 PG to operate a semaphore and either be in locations of waiting, critical section, or waiting for access. Then carry out parallel composition by performing incomplete interleaving and then eliminating unreachable locations.
