Information Technology Reference
In-Depth Information
2 The LogFire DSL
In this section we shall illustrate LogFire by specifying a monitor for the re-
source management system for a planetary rover. Subsequently we will briefly
explain the operational meaning of the specification.
2.1 Specification
Consider a rover that runs a collection of tasks in parallel. A resource arbiter
manages resource allocation, ensuring for example that a resource is only used
by one task at a time. Consider that we monitor logs containing the events:
grant
(
t,r
):task
t
is granted resource
r
.
release
(
t,r
):task
t
releases resource
r
.
end
() : the end of the log is reached.
Consider next the following informal requirement that logs containing instances
of these event types have to satisfy:
“A resource can only be granted to one task (once) at any point in time,
and must eventually be released by that task.”
We shall now formalize this requirement as a LogFire monitor. The main com-
ponent of LogFire is the class
Monitor
, which any user-defined monitor must
extend to get access to constants and methods provided by LogFire.User-
defined monitors will contain rules of the form:
name
--
condition
1
&
...
&
condition
n
|->
action
A rule is defined by a name, a left hand side consisting of a conjunction of con-
ditions, and a right hand side consisting of an action to be executed if all the
conditions match the fact memory. A condition is a pattern matching facts or
events in the fact memory, or, as we shall later see, the negation of a pattern,
being true if such a fact does not exist in the fact memory. Arguments to condi-
tions are variables (quoted identifiers of the type
Symbol
) or constants. The first
occurrence of a variable in a left-hand side condition is binding, and subsequent
occurrences in that rule much match this binding. An action can be adding facts,
deleting facts, or generally be any Scala code to be executed when a match for
the left-hand side is found. Our monitor becomes:
class
ResourceProperties
extends
Monitor
{
val
grant, release , end = event
val
Granted = fact
”
r1
”
−−
grant('t, 'r) & not(Granted('t, 'r))
|
−
>
Granted('t, 'r)
”
r2
”
−−
Granted('t, 'r) & release('t, 'r)
|
−
>
remove(Granted)
”
r3
”
−−
Granted('t, 'r) & grant(' ,'r)
|
−
>
fail(
”
double grant
”
)
”
r4
”
−−
Granted('t, 'r) & end()
|
−
>
fail(
”
missing release
”
)
”
r5
”
−−
release('t,'r) & not(Granted('t,'r))
|
−
>
fail(
”
bad release
”
)
}
