Synthesising Analysers¶

Trace events, in practice¶

When it comes to tooling, the representation of trace events tends to be implementation-specific and is often tied to the chosen language framework. To disentangle the specification and analysis concepts, detectEr employs the intermediate representation seen earlier, consisting of the program events, fork, init, exit, send and recv. These intermediate events are internally translated to the ones that the native Erlang tracing infrastructure uses. We adopt this approach since it simplifies the implementation of analysers.

From specification to analyser¶

To demonstrate how you can use detectEr to synthesise analysers, we use the formalisation of property P₃ as a vehicle. detectEr Linear Time provides the maxhml_eval:compile/2 function that compiles maxHML specifications to executable Erlang code. The compile function accepts two arguments, the path that points to the maxHML script file, and a list of options that control how the resulting analyser is generated. maxHML script files are plain text formatted files with a .hml extension, and must at least contain one specification. Multiple specifications are separated with comma, and every file must be terminated with a full-stop. The configuration options that maxhml_eval:compile/2 are as follows.

Option	Description
`outdir`	Directory where the synthesised analyser file should be written. If left unspecified, defaults to the current directory `.`.
`erl`	Instructs `compile` function to output the synthesised analyser as Erlang source code rather than in `beam` format. If left unspecified, defaults to `beam`.

Analysers are synthesised from the Erlang shell, which needs to have the detectEr binaries loaded in its code path. This is done by launching the shell with the -pa flag. For this example, we change the directory to examples/erlang and launch the Erlang shell, of course assuming that the detectEr source files have already been compiled. Refer to the section Setting up detectEr Linear Time if you need to do this.

[duncan@local]:$ cd examples/erlang
[duncan@local]:$ erl -pa ../../detecter/ebin
Erlang/OTP 23 [erts-11.2.1] [source] [64-bit] [smp:4:4] [ds:4:4:10] [async-threads:1] [hipe] [dtrace]
Eshell V11.2.1  (abort with ^G)
1>

With the Erlang shell loaded, compile the prop_no_leak.hml.

1> maxhml_eval:compile("props/prop_no_leak.hml", [{outdir, "ebin"}, erl]).
ok

We have specified the erl option to generate the analyser source code in order to overview the internal workings of analysers. You may skip this section if you want just learn how to to use the tool.

So the first thing that we should note is that the analyser is one higher-order function returns other functions or atoms in turn. The init, send, recv event patterns in the specification are translated by maxhml_eval:compile/2 to the event format that the EVM uses for tracing. These event mappings are tabled below.

Program event	Pattern	EVM trace event translation
`fork`	`P₁` → `P₂`, `Mod`:`Fun`(`Args`)	`{trace, P₁, spawn, P₂, {Mod, Fun, Args}}`
`init`	`P₁` ← `P₂`, `Mod`:`Fun`(`Args`)	`{trace, P₁, spawned, P₂, {Mod, Fun, Args}}`
`exit`	`P₁` ** `Reason`	`{trace, P₁, exit, Reason}`
`send`	`P₁` : `P₂` ! `Msg`	`{trace, P₁, send, Msg, P₂}`
`recv`	`P₂` ? `Msg`	`{trace, P₁, 'receive', Msg}`

The entry point to analysers is the hardcoded function mfa_spec/1 that accepts as an argument the function that we designated with the keyword with, line 5. We revisit mfa_spec/1 when we discuss the instrumentation. In the specific case of our token server example, the targeted function on line 5 is loop in the token_server module. Our examples packaged with the detectEr distribution include a second implementation of a buggy token server which we will use to show how analysers flag rejection verdicts. prop_no_leak.hml specifies the same formalisation of P₃ for this buggy version.

We will use this buggy version of the token server to show how a rejection verdict is reached when the incorrect behaviour in the program trace is detected.

Executable analysers¶

We can go ahead and recompile prop_no_leak.hml script, this time removing the erl option.

Of course, the resulting analyser binary must be included in the code path of the program we are running, together with the detectEr binaries.

2> maxhml_eval:compile("props/prop_no_leak.hml", [{outdir, "ebin"}]).
ok

Now we look at how we instrument the system with monitors.