Causality Analysis

Question

Hi,

I have to question to the solution of a task from the 2020 exam.

The task here is to do a causality analysis for the first macro step with i=0.

Step 0 is clear, but step 1 is not clear for me. E(o2) is 0 because emit(o2) is not

in D_can. But now according to my understanding emit(o1) should also be

in D_must because the first if-statement is then true. Then E(o1) would be 1 in

step 2.

I hope you can explain to me what I am doing wrong.

Answer 1

There are different ways to reason about this; you may argue with the guarded actions or with the SOS semantics which is the intention of the exercise. Let's first consider the guarded action approach: The program has the following guarded actions:

    o1&!o2&st => o1 = true
    i&o1&!o1&st => o2 = true
    o1&i&l&!o1 => o2 = true

At starting time, we have st=1 and l=0, so that we get the following reduction:

    o1&!o2 => o1 = true
    i&o1&!o1 => o2 = true
    0 => o2 = true

For input i=0, we moreover get

    o1&!o2 => o1 = true
    0 => o2 = true
    0 => o2 = true

Now, we evaluate the guards with E(o1)=E(o2)=⊥, and obtain

    ⊥ => o1 = true
    0 => o2 = true
    0 => o2 = true

Hence, whether o1=true may be fired or not is not clear at this point of time. This action is in the CAN set, but not in the MUST set, and we can therefore not change the value of o1. Moreover, no action on o2 can be fired, so that the reaction to absence determines the value of o2, and thus o2=0, and thus !o2=1, and we then get

    o1 => o1 = true
    0 => o2 = true
    0 => o2 = true

Thus, the value of o1 cannot be determined.

The approach using the SOS reaction rules computes for E(o1)=⊥ and E(o2)=0 at first for "if(!o2) emit(o1);" the actions Dmust=Dcan={emit(o1)} and this is also obtained for the entire body of the immediate abort statement. However, then we have to consider the SOS rules for the strong immediate abort statement "immediate abort S when(!o1);". Since the abort condition is ⊥, it will empty the must set and will leave the can set as it is. Hence, emit(o1) remains in the can set, but is removed from the must set. Again, we cannot make further progress from here.

Comments

The above reduction of the guarded action for o2 is:
i&o1&!o1 => o2 = true
0 => o2 = true

Hence, o2 is always false regardless of the input, right?

But emit(o2) is in the CAN set in the solution of task b), where we have the input i=1.
Shouldn't it be again Dcan={emit(o1)}?

---

No that is not the case. Output o2 is false when i is false, but if i is true, then o2 does not make it to false in teh first step. To see this, recall that the program has the following three guarded actions:

    o1&!o2&st => o1 = true
    i&o1&!o1&st => o2 = true
    o1&i&l&!o1 => o2 = true

For i=0, st=1, and l=0, this reduces to

    o1&!o2 => o1 = true
    0 => o2 = true
    0 => o2 = true

So that o2 becomes false by reaction-to-absence, since there is no action on o2 that can fire. With o2=false, we finally get o1 => o1 = true with current value o1=⊥ which gets stuck with that value.

For i=1, st=1, and l=0, this reduces to

    o1&!o2 => o1 = true
    o1&!o1 => o2 = true
    0 => o2 = true

which becomes with values o1=o2=⊥

    ⊥ => o1 = true
    ⊥ => o2 = true
    0 => o2 = true

Here, o2 may still become true if the guard of the second guarded action could switch from ⊥ to true. Output o2 is therefore still in the CAN set but not in the MUST set, and the same is the case for output o1.

You may try this also with the simulator using the following driver:

    module Problem7a (event ?i,o1,o2) {
        immediate abort {
            if(!o2) emit(o1);
            l: immediate await(i);
            if(!o1) emit(o2);
        } when(!o1);
    }
    drivenby t0 {
        i=false;
        pause;
    }

Bytheway, looking at your very first question: For the emit(o1) statement to fire, it is not enough that !o2 holds (as the if-statement suggests). There is also an immediate abort... when(!o1) around so that we need o1&!o2 in the first step to fire emit(o1).

---

Thank you, now I understand the reason for Dcan={emit(o1),emit(o2)}.