Lectures 9 and 10: 29th October 2019 Flashcards Preview

CS4052 Logic and Software Verification > Lectures 9 and 10: 29th October 2019 > Flashcards

Flashcards in Lectures 9 and 10: 29th October 2019 Deck (47)
Loading flashcards...
1

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

2

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

3

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

4

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.

5

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.

6

How does parallel composition work with TSes?

Doesn't - may only be done with PGs

7

What is interleaving?

Composing combinations of actions by different program processes, examining only their effects on their local variables (doesn't handle globals).

8

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 --α--> 1 s’1
-------------------------------
⟨s1, s2⟩ --α--> ⟨s’1, s2⟩

and

s2 --β--> 2 s’2
-------------------------------
⟨s1, s2⟩ --β--> ⟨s1, s'2⟩

and L(⟨s1, s2⟩) = L1(s1) ∪ L2(s2)
for α ∈ Act1, β ∈ Act2

9

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

????????

10

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 --g:α--> 1 l’1
-------------------------------
⟨l1, l2⟩ --g:α--> ⟨l’1, l2⟩

and

l2 --g:β--> 2 l’2
-------------------------------
⟨l1, l2⟩ --g:β--> ⟨l1, l’2⟩

and Effect(α, η)(v) = Effecti(α, η)(v) if α ∈ Acti, v ∈ Vari

11

When would you interleave PGs?

When interleaving programs with shared variables

12

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.

13

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.

14

How is interleaving different for PGs and TSes?

Interleaved PGs can't interfere with global variables but this is possible in interleaved TSes.

15

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.

16

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

17

What are critical actions in composed PGs?

Actions that access global variables are critical. Critical actions cannot be executed simultaneously.

18

What are composed PGs?

A PG resulting from the parallel composition of two other PGs

19

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.

20

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.

21

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.

22

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.

23

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.

24

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.

25

How do you prove which states in a composed graph are reachable?

For all transitions, check the state of variables before them and after them for the process associated with the transition by building its variable states from the root/initial states. If the conditions of the transition would not allow them from the initial variable values then eliminate the transition.

26

How does parallel composition work for PGs?

Make locations as the cartesian product: each possible combination group of states in each process. Make each transition according to each new location based on the process changing in them, and then eliminate unreachable states.

27

What is handshaking?

When perfectly synchronised communications between interleaved processes lead to them performing actions simultaneously

28

What does the handshaking operation do?

Perform interleaving on TSes or PGs and then consider actions for transitions. If their actions are independent then leave them, but otherwise if guard makes them dependent then if they both happen then ensure they both take effect simultaneously.

29

How is the handshaking operation notated?

Let TSi=(Si, Acti,Ti, Ii, APi, Li), i=1,2 be transition systems and H⊆Act1∩Act2 with τ∉H. TS1 ||H TS2 is:

TS1 ||H TS2 = (S1 × S2, Act1 ∪ Act2, T, I1 × I2, AP1 ∪ AP2, L)

L(⟨s1, s2⟩) = L1(s1) ∪ L2(s2)

T is such that:

if an action, α, is in both and can be executed in a transition from the current states of both TSes (synchronisation):

s1 -α-> 1 s’1 ⋀ s2 -α->2 s’2
given that:
⟨s1,s2⟩ -α-> ⟨s’1,s’2⟩

i.e. that if you can transition from start locations from the interleaved TSes - with actions in both languages and from both start states - both transitions occur simultaneously

else then act as interleaving, i.e. perform the action with 1 TS without affecting the other/s:

s1 -α-> 1 s’1 given that ⟨s1, s2⟩ -α-> ⟨s’1, s2⟩
and
s2 -α-> 2 s’2 given that ⟨s1, s2⟩ -α-> ⟨s1, s’2⟩

30

How are the conditions for interleaving and synchronisation different?

if an action, α, is in both and can be executed in a transition from the current states of both TSes with synchronisation (otherwise falling back to interleaving):

s1 -α-> 1 s’1 ⋀ s2 -α->2 s’2
given that:
⟨s1,s2⟩ -α-> ⟨s’1,s’2⟩

i.e. that if you can transition from start locations from the interleaved TSes - with actions in both languages and from both start states - both transitions occur simultaneously

with interleaving, i.e. perform the action with 1 TS without affecting the other/s:

s1 -α-> 1 s’1 given that ⟨s1, s2⟩ -α-> ⟨s’1, s2⟩
and
s2 -α-> 2 s’2 given that ⟨s1, s2⟩ -α-> ⟨s1, s’2⟩