Verdict Explainability¶

An example¶

Let us briefly review the property prop_no_leak.hml, that expresses:

(P₃) The token 1 is not leaked by the server in reply to a client request.

with
  token_server:loop(_, _)
check
  [{_ <- _, token_server:loop(OwnTok, _)}]
  max(X.
    [{_ ? _}](
      [{_:_ ! Tok when OwnTok =:= Tok}]ff
      and
      [{_:_ ! Tok when OwnTok =/= Tok}]X
    )
  ).

The corresponding high-level description of the monitor generated by maxhml_eval:compile/2 is as follows.

{_ <- _, token_server:loop(OwnTok, _)}.rec X(
  {_ ? _}(
      {_:_ ! Tok when OwnTok =:= Tok}.no
      +
      NOT*{_:_ ! Tok when OwnTok =:= Tok}*.yes
    and
      {_:_ ! Tok when OwnTok =/= Tok}.X
      +
      NOT*{_:_ ! Tok when OwnTok =/= Tok}*.yes
  )
  +
  NOT*{_ ? _}*.yes
)
+
NOT*{A <- B, token_server:loop(OwnTok, _)}*.yes

In this high-level description, we use + to denote a mutually-exclusive choice between two branches of the monitor, and NOT* ... * to designate the monitor branch where (i) either the specified action pattern does not match the actual event from the trace, or, (ii) the pattern matches, but the Boolean constraint is not satisfied, given the data inside the variables contained in the pattern. Parallel conjunctions are written as and, recursion is denoted by rec, and yes and no respectively denote the verdicts that monitors flag.

Monitor reduction, step-by-step¶

Recall the monitor:

{_ <- _, token_server:loop(OwnTok, _)}.rec X(
  {_ ? _}(
      {_:_ ! Tok when OwnTok =:= Tok}.no
      +
      NOT*{_:_ ! Tok when OwnTok =:= Tok}*.yes
    and
      {_:_ ! Tok when OwnTok =/= Tok}.X
      +
      NOT*{_:_ ! Tok when OwnTok =/= Tok}*.yes
  )
  +
  NOT*{_ ? _}*.yes
)
+
NOT*{A <- B, token_server:loop(OwnTok, _)}*.yes

Let us assume that our buggy version of the token server exhibited the execution below. For this sequence of events, we describe the monitor reduction that explains how a verdict is reached.

1
2
3

{trace,<0.84.0>,spawned,<0.82.0>,{token_server,loop,[1,1]}}
{trace,<0.134.0>,'receive',{<0.136.0>,0}}
{trace,<0.134.0>,send,1,<0.136.0>}

The monitor analyses the event {trace,<0.84.0>,spawned,<0.82.0>,{token_server,loop,[1,2]}} and it chooses the left branch {A <- B, token_server:loop(OwnTok, _)} since the pattern matches, and its Boolean constraint true (elided) is always satisfied. The residual monitor with the instantiated data of OwnTok = 1.

rec X(
  {_ ? _}(
      {_:_ ! Tok when 1 =:= Tok}.no
      +
      NOT*{_:_ ! Tok when 1 =:= Tok}*.yes
    and
      {_:_ ! Tok when 1 =/= Tok}.X
      +
      NOT*{_:_ ! Tok when 1 =/= Tok}*.yes
  )
  +
  NOT*{_ ? _}*.yes
)

It then performs an internal transition to unfold the recursive variable X (expansion is not shown in the monitor due to space reasons).

{_ ? _}(
    {_:_ ! Tok when 1 =:= Tok}.no
    +
    NOT*{_:_ ! Tok when 1 =:= Tok}*.yes
  and
    {_:_ ! Tok when 1 =/= Tok}.X
    +
    NOT*{_:_ ! Tok when 1 =/= Tok}*.yes
)
+
NOT*{_ ? _}*.yes

It analyses {trace,<0.134.0>,'receive',{<0.136.0>,0}}, and choosing the left monitor branch. The left monitor branch matches any receive event, which means that the right branch matches no receive event.

  {_:_ ! Tok when 1 =:= Tok}.no
  +
  NOT*{_:_ ! Tok when 1 =:= Tok}*.yes
and
  {_:_ ! Tok when 1 =/= Tok}.X
  +
  NOT*{_:_ ! Tok when 1 =/= Tok}*.yes

At this point, the two conjuncted sub-monitors can evolve in parallel, given the trace event {trace,<0.134.0>,send,1,<0.136.0>}. The left sub-monitor {_:_ ! Tok when 1 =:= 1}.no + NOT*{_:_ ! Tok when 1 =:= 1}*.yes chooses the left branch since the pattern matches and the Boolean constrain is fulfilled. The right sub-monitor {_:_ ! Tok when 1 =/= 1}.X + NOT*{_:_ ! Tok when 1 =/= 1}*.yes chooses the right branch since the pattern matches, but the Boolean constrain for the right branch is satisfied. This reduces the monitor to:
1 2 3
no and yes
The last internal computation leads the monitor to the rejection verdict no.

Try this for yourself¶

detectEr Linear Time includes the function lin_analyzer:analyze_trace/2 to reduce a monitor, given a trace of events. In this example, we use the monitor that we synthesised earlier for P₃. This is located in the script props/prop_no_leak.hml.

First we invoke the main monitor function prop_no_leak:mfa_spec/1 to obtain the monitor instance. Since we need to match the pattern expected by mfa_spec, i.e., {token_server,loop,[_,_]}, we can use any arguments we wish. In this example, we shall use 1 for both tokens.
```
1> {ok, Mon} = prop_no_leak:mfa_spec({token_server,loop,[1,1]}).
...
```
Note that prop_no_leak:mfa_spec/1 returns the tuple tagged with ok, and we unwrap it accordingly to obtain the monitor in #1erlang Mon.

Next, we create the trace to feed to the monitor as a list of events:

2> Trc = [{trace,<0.84.0>,spawned,<0.82.0>,{token_server,loop,[1,1]}},
{trace,<0.134.0>,'receive',{<0.136.0>,0}},
{trace,<0.134.0>,send,1,<0.136.0>}].

Finally the trace can be analyzed using the following invocation:
```
3> {PdList, _}= lin_analyzer:analyze_trace(Trc, Mon).
```
Variable PdList contains the whole justification that details the steps taken by the monitor to reach the violation verdict no.
The lin_analyzer module also provides the means to pretty print the contents of the proof derivation list PdList.
```
4> lin_analyzer:show_pdlist(PdList).
```

Step 4 shows that the monitor is reduced using the following operational semantic rules:

Rule mChsL on {trace,<0.84.0>,spawned,<0.82.0>,{token_server,loop,[1,1]}}.

1.1. Axiom mAct on {trace,<0.84.0>,spawned,<0.82.0>,{token_server,loop,[1,1]}}.
Axiom mRec on tau.
Rule mChsL on {trace,<0.134.0>,'receive',{<0.136.0>,0}}.

3.1. Axiom mAct on {trace,<0.134.0>,'receive',{<0.136.0>,0}}.
Rule mPar on {trace,<0.134.0>,send,1,<0.136.0>}.

4.1. Rule mChsL on {trace,<0.134.0>,send,1,<0.136.0>}.

4.1.1. Axiom mAct on {trace,<0.134.0>,send,1,<0.136.0>}.

4.2. Rule mChsR on {trace,<0.134.0>,send,1,<0.136.0>}.

4.2.1. Axiom mAct on {trace,<0.134.0>,send,1,<0.136.0>}.
Rule mConYR on tau.

For the complete reference of these operational rules, please refer to the companion paper.