Quickstart¶
Launching detectEr from the shell¶
The detecter/ebin
directory created previously needs to be included in the Erlang runtime path to preload all the binaries required to be able to use detectEr.
This is done by using the -pa
switch when launching the Erlang shell.
[duncan@local]:$ erl -pa /path/to/detecter/ebin
Once loaded, detectEr can be used to monitor systems that execute on the Erlang Virtual Machine. It also supports the monitoring of systems that run outside of the EVM, provided that these record their logs in files following a predetermined formatting that enables detectEr to extract runtime information. This topic is covered in more depth in the Instrumentation section. For now, we establish the workflow required to use detectEr by way of the traditional ‘hello world’ example.
Hello world¶
Before using detectEr, you should get an intuitive grasp of what monitoring is, and the steps one needs to follow to initialise and start the monitoring process. If this is your first time using Erlang, the following wil help you get acquainted with the Erlang shell.
Launch a new terminal emulator window (e.g. Terminal on Ubuntu or macOS), navigate to the root detectEr directory, and:
-
Change the directory to
examples/erlang
.[duncan@local]:/detecter$ cd examples/erlang [duncan@local]:/detecter/examples/erlang$ ls -l -rw-rw-r-- 1 duncan duncan 996 May 17 17:16 Makefile drwxrwxr-x 2 duncan duncan 4096 May 17 17:16 props drwxrwxr-x 3 duncan duncan 4096 May 17 17:16 src
-
Execute
make
to compile all of the Erlang source code modules located inexamples/erlang/src
. A newebin
directory containing the compiled*.beam
files is created. BEAM files are (fairly) portable binaries consisting of bytecode that is interpreted by the EVM, similar to how Java operates.3. Launch the Erlang shell[duncan@local]:/detecter/examples/erlang$ make rm -f ebin/*.beam ebin/*.E ebin/*.tmp erl_crash.dump ebin/*.app ... [duncan@local]:/detecter/examples/erlang$ ls -l -rw-rw-r-- 1 duncan duncan 996 May 17 17:16 Makefile drwxrwxr-x 7 duncan duncan 224 May 17 17:16 ebin drwxrwxr-x 2 duncan duncan 4096 May 17 17:16 props drwxrwxr-x 3 duncan duncan 4096 May 17 17:16 src
erl
. We add the binaries of theebin
directory to the Erlang code path via the-pa
flag to load and make them accessible from the shell.4. The Erlang shell allows you to type expressions and execute them by pressing Enter. Every expression typed on the shell must be terminated with a full-stop. Try invoking the function[duncan@local]:/detecter/examples/erlang$ erl -pa 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>
greet
of thehello
module. The functiongreet
accepts one argument, the name of the person to greet, specified as a string enclosed within double quotes.5. Quit the Erlang shell by typing1> hello:greet("Duncan"). Hello there, Duncan! ok 2>
q().
Function signatures
In Erlang (and Elixir), functions are uniquely identified via the triple mod:fun/arity
, where mod
is the module name, fun
, the name of the function contained in the module, and arity
, the number of arguments that the function accepts.
This reference format is commonly known as MFA.
For example, our greet
function inside the module hello
can be concisely referred to as hello:greet/1
.
We refer to functions in the same module simply as fun/arity
.
Hello world, the asynchronous way¶
You might have noticed that hello:greet/1
pauses the Erlang shell momentarily before the greeting is displayed.
During this interval, the shell is inoperable and cannot accept user input.
Such function calls are called synchronous invocations, since they block the caller until the called function returns, i.e. the body of the called function is executed in its entirety and a value is returned to the caller.
Examining the body of greet
below makes it clear why the Erlang shell stops responding when the function call is effected.
1 2 3 |
|
Line 1
defines the function greet
that accepts Name
as parameter, while line 3
prints the greeting on the Erlang shell via call to io:format/2
.
The call timer:sleep(5000)
on line 2
pauses the caller process (i.e. the Erlang shell, in this case) for 5000
ms before executing the rest of the function body.
In Erlang, the function return value is the result of the last expression in the function body; for the case of greet
, this value is the atom ok
that is returned by io:format/2
.
Synchronous calls
Synchronous function calls are useful when one needs to ensure that certain processes execute in some prescribed order with respect to one another, e.g. in lock step. This mode of interaction is common to many standard communication protocols such as HTTP, SMTP, DNS, etc.
Unwanted synchrony can be easily avoided by launching functions to execute as independent processes that run concurrently with other processes in the system.
To this end, Erlang provides the Built-in Functions spawn/{1-4}
, and their variations.
We slightly tweak our hello world example to spawn hello:greet/1
as a separate process that executes concurrently with the Erlang shell process.
4 5 |
|
The function start_greet/1
implements this modification.
It uses the BIF spawn/3
(line 5
) to launch hello:greet/1
as a process, returning the new process ID.
Process IDs (PIDs for short) are triples of the form <A.B.C>
that uniquely identify Erlang processes executing on the EVM.
spawn/3
is parametrised by the module name, the name of the function to spawn, and the list of arguments accepted by the function.
Function start_greet/1
makes use of the predefined macro ?MODULE
, that gets replaced with the name of the module it appears in when the source code of the hello
module is preprocessed by the Erlang compiler.
Concretely, the invocation to spawn/3
on line 5
yields the source code spawn(hello, greet, [Name])
prior to compilation.
Restart the Erlang shell and invoke hello:start_greet/1
.
1> hello:start_greet("Duncan").
<0.97.0>
Hello there, Duncan! % Shown after a slight pause.
2>
Observe that now:
-
The return value of
start_greet
is the PID of the spawned process<0.97.0>
instead of the atomok
; -
The Erlang shell does not block, but returns immediately;
-
After the predefined sleep time elapses, the greeting is printed to the shell.
Outline runtime monitoring¶
In this quickstart demo, we monitor the execution of our asynchronous hello world example using the outline form of instrumentation.
-
Launch the shell as previous, adding the hello world binaries in
ebin
to the Erlang code path. The detectEr binaries compiled earlier are also included.[duncan@local]:/detecter/examples/erlang$ erl -pa ebin ../../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>
-
Compile the sample
prop_hello.hml
property script to generate the corresponding analyser binary.1> hml_eval:compile("props/prop_hello.hml", [{outdir,"ebin"}, v]).
This compilation procedure, known as the synthesis, translates sHML specifications written in
*.hml
script files to their analyser equivalents. For now, it suffices to know that sHML—the logic used by detectEr—expresses properties of the system one wishes to runtime verify. Our analyser Erlang binary generated from the sample property is placed in/detecter/examples/erlang/ebin
and automatically loaded for use in the shell code path.2> ls("ebin"). hello.beam prop_hello.beam ...
The analyser
prop_hello
exposes a single function,mfa_spec/1
, that accepts the MFArgs triple{Mod, Fun, Args}
designating the Erlang process to be analysed. Specifically,Mod
,Fun
andArgs
are the components of the function passed as arguments tospawn/3
. For our hello world example,Mod
is the atomhello
,Fun
is the function namegreet
, andArgs
, the singleton argument list containing the name of the person to be greeted. You can testprop_hello:mfa_spec/1
analyser function by providing the triple{hello, greet, ["Duncan"]}
.3> prop_hello:mfa_spec({hello, greet, ["Duncan"]}). *** [<0.82.0>] Instrumenting monitor for MFA pattern '{hello, greet, ["Duncan"]}'. *** [<0.82.0>] Reached verdict 'no'.
-
Launch the monitored system.
4> monitor:start_online({hello, start_greet, ["Duncan"]}, fun prop_hello:mfa_spec/1, []).
The function
monitor:start_online/3
accepts three arguments: a MFArgs describing the function that is to be spawned as an Erlang process, the analyser function, and a list of options. Setting MFArgs to{hello,start_greet,["Duncan"]}
and the analyser tofun prop_hello:mfa_spec/1
launches the hello world and analyser processes to execute concurrently.
In this introductory example, the analyser prop_hello
promptly terminates with the verdict no
as soon as our hello world program starts executing.
The no
verdict informs us that a program has violated the specification of prop_hello.hml
.
We next look at a typical concurrent program where processes interact, and study what kind of useful properties one might want such systems to observe.