Model-Based Specification
Martin Sulzmann
Motivation
Who cares?
No need. We know how to program. Whatever we need we find via 'google' ...
"Informatik" = Information + Automation
Goal:
Understand the problem (Analysis)
Code up a solution (Implementation)
Make sure that the solution is correct and matches the problem (Verification + Validation)
Verification:
Validation:
Terminology:
- System: Refers to the product. As we focus on software aspects, in our case consists of program code. Can be rather complex as the program code may run on several machines, remotely, web-based etc. There may be interactions among sub-systems etc. Usually, it is a system of systems!
Example
The problem description says:
The increment function shall increment each value by one.
The specification given to the programmer says:
For each int value, the function shall produce some int value.
The programmer implements.
inc (x int) int {
return 0
}
So, verification succeeds but validation fails.
Modeling
Often phrased as model-based software development.
Purpose:
Assist implementation and specification tasks.
Avoid coding errors.
Make use of high-level abstractions.
Make model easy to extend, maintain, ...
What is a (formal) model? Comes in all shapes and sizes.
Important We expect that for any model we find a concise semantic description (so we actually know what a specific model means!)
Examples:
The programming language C is a low-level programming model. Great for low-level stuff but prune to tricky to spot programming mistakes.
Some of you find that Java is a much better, more high-level programming model. Some coding errors can't happen in the first place (think of memory management). Also, Java offers higher level of abstractions (classes, ...). This can be useful to achieve a solution which is easier to maintain, ...
Textual versus graphical models:
Any programming language serves as a text-based modeling language. For example, Perl is a great language for write scripts. The modeling focus there is on scripting tasks.
We will also encounter graphical modeling languages. For example, automata-based models. Some programing languages offer a graphical interface.
Logic-based models:
What about UML?
- Well, UML offers a wide range of models. My main criticism is that these models often lack some formal underpinnings. So we won't directly discuss UML here.
Specification
- Make use of a formal model to describe the intended behavior of your system.
Important:
We can use the same type of model to describe the actual working of the system (its implementation) and its specification.
Extreme case. The implementation serves as the specification! Does this make sense?
Common approach:
State-Based Modeling
Finite State Machines (FSM)
We consider a number of examples where FSM are useful for modeling the system's behavior.
"Hirte-Wolf-Kohl-Ziege"
Modeling with finite state machines
see black board
"count"
Modeling with Mealy/Moore machines (input as well as output).
Application: Generation of test cases.
see black board
We use the "count" finite state machine (FSA) for validation.
From the FSA we generate some C code (see below).
We verify that the C code conforms to the FSA specification.
Zustandsbasierte Modellierung
#include "stdio.h"
/*
1. Woerter in einem String zaehlen.
Was ist ein Wort?
Wir definieren ein Wort als eine Sequenz von
Zeichen welche nicht getrennt ist durch Leerzeichen.
2. Zustands-basierte Modellierung.
Wir definieren unser Alphabet als die Menge
Sigma = { CH, EOS, WS }
wobei
EOS = Nullterminator
WS = Leerzeichen ('white space')
CH = Zeichen ('character')
Die Menge von Zustaenden und Transitionen ist wie folgt.
1 -- WS --> 1
1 -- EOS --> 2
1 -- CH --> 3
3 -- WS --> 1
3 -- CH --> 3
3 -- EOS --> 2
Menge von Zustaenden ist {1,2,3}
1 ist der Startzustand
3 ist der Finalzustand
Obiger Automat ist ein Beipsiel eines endlichen Automaten.
3. Zaehlen von Woertern.
Um die Woerten zu zaehlen, benoetigen wir neben einer Eingabe (Zeichen WS, CH, EOS)
auch eine Ausgabe (Anzahl der gefunden Woerter).
Dazu koennen wir einen Mealy/Moore Automaten verwenden.
Z.B. im Fall eines Mealy Automaten koennen wir auf die Transition eine Ausgabe legen.
Notation.
Wir schreiben
state1 -- In / Out --> state2
Fuer einen Uebergang von Zustand state1 nach Zustand state2,
falls das aktuelle Eingabesymbol In ist.
Als Ausgabe finden wir Out.
Ein Mealy Automate liefert einen Trace von Ausgabesymbolen.
Wir benutzen zur Vereinfachung eine Zustandsvariable.
-- / cnt=0 --> 1
1 -- WS --> 1
1 -- EOS --> 2
1 -- CH / cnt++ --> 3
3 -- WS --> 1
3 -- CH --> 3
3 -- EOS --> 2
*/
// Implementierung 1
char* scanWS(char* s) {
while(*s == ' ') {
s++;
}
return s;
}
int isCH(char c) {
return (c != ' ' && c != '\0');
}
char* scanCH(char* s) {
while(isCH(*s)) {
s++;
}
return s;
}
int countWords(char* s) {
int cnt = 0;
s = scanWS(s);
while(isCH(*s)) {
cnt++;
s = scanCH(s);
s = scanWS(s);
}
return cnt;
}
// Implementierung 2
// Direkte Umsetzung des Modells.
int countWordsModell(char* s) {
int state = 1;
int cnt = 0;
while(1) {
switch(state) {
case 1:
if(*s == ' ')
state = 1;
if(*s == '\0')
state = 2;
if(isCH(*s)) {
cnt++;
state = 3;
}
break;
case 2:
return cnt;
case 3:
if(*s == ' ')
state = 1;
if(*s == '\0')
state = 2;
if(isCH(*s))
state = 3;
break;
} // switch
s++; // next symbol
} // while
}
int main() {
// Write your own tests and use cases :)
return 1;
}
Communicating Finite State Machines (CFSM)
Communication among FSM. How?
Transitions with input and output actions.
Synchronization via hand-shake.
Definition
Let C be a finite alphabet of channel names.
For each x in C, we refer to x! as an output action over channel x and
to x? as an input action over channel x.
Let S be a finite set of states. We generally use symbols p,q to refer to states.
We define a CFSM = (M_1, ..., M_n) as an n-tuple of finite state machines M_i.
Each finite state machine M consists of
(1) a finite set of states S where there is a designated starting state,
written M.init, and
(2) a finite set of transitions of the following three forms
p ----> q
p -x!-> q
p -x?-> q
where x in C and p,q in S.
We refer to the first kind as an "epsilon" transition
and to the second and third kind, as output and input
transitions respectively
Let p_i be a state of the FSM M_i.
We refer to (p_1, ..., p_n) as a (state) configuration of the CFSM.
We refer to (M_1.init, ..., M_n.init) as the initial configuration of the CFSM.
Execution proceeds by rewriting configurations which boils
down to executing transitions of the individual FSM.
Epsilon transitions can be executed spontaneously whereas
input and output transititions require synchronization.
(p_1, ..., p_i, ..., p_n) -----> (p_1, ..., q_i, ..., p_n)
if we find p_i -----> q_i in M_i
(p_1, ..., p_i, ..., p_j, ..., p_n) --x--> (p_1, ..., q_i, ..., q_j, ..., p_n)
if either p_i -x!-> q_i in M_i and p_j -x?-> q_j in M_j
or p_i -x?-> q_i in M_i and p_j -x!-> q_j in M_j
We refer to a path as a sequence of execution steps starting from the initial configuration.
There may be several (alternative) paths and paths may not be finite (there are no final states).
We can represent all possible execution steps as a tree-like structure where the
root represents the initial configuration.
Examples
"black-board"
Go versus CFSM
"black-board"
Temporal specification
Motivation
Specify the behavior of a system over time.
Timed Computation Tree Logic (TCTL)
Specify the (expected) behavior of a CFSM in terms of the tree-like structure which is obtained by execution of the CFSM.
Definition
TCTL ::= A[] B
| A<> B
| E[] B
| E<> B
| B --> B
B ::= SomeAtomicProposition
| B and B
| B or B
| B imply B
| not B
| (B)
B makes statements about configurations, for example
M_1.init and M_2.exit
M_1 is in the initial state and M_2 ist in the exist state
Informal semantic meaning:
A for all paths
E for at least one path
[] for all configurations
<> for at least one configuration
Considering the specific cases.
A[]B For all paths and configurations along each path B holds.
A<>B For all paths there is at least one configuration for which B holds.
E[]B There exists a path and along that path,
for all configurations B holds.
E<>B There exists a path and along that path,
for at least one configuration B holds.
Special case:
B1 --> B2 = A[] (B1 imply A<> B2)
For all paths, if we encounter a configuration for which B1 holds,
then for all paths which continue from that configuration,
we must find a configuration where B2 holds.
Safety versus Liveness
Safety = Something bad never happens.
A[] B Invariant
E[] B Some "safe" path exists
Liveness = Something good will eventually happen.
A<> B We eventually reach "B"
B1 --> B2 "B1" eventually leads to "B2"
Algebraic Laws
not A [] B = E <> not B
not A <> B = E [] not B
not E [] B = A <> not B
not E <> B = A [] not B
Linear Temporal Logic (LTL)
Specify the (expected) behavior of a CFSM in terms of the traces which are obtained by execution of the CFSM.
Definition
Trace = sequence of synchronization points = channel names.
We write "config" to denote a configuration where config_0
represents the initial configuration.
Consider the path
config_0
--x_1-->
config_1
--x_2-->
....
Then, the trace implied by the above path consists of
x_1 x_2 ...
Recall that paths are infinite (and so are traces!).
LTL is a form of linear logic which states properties about the traces which are obtained by execution of the CFSM.
L ::= x where x in C
| L /\ L
| L \/ L
| ! L
| globally L
| eventually L
| L until L
| next L
| (L)
LTL infinite trace semantics.
Let w be an infinite sequence of channel names.
We write w^i to denote the trace obtained by dropping the first i channels.
We write w[i] to refer to the i-th position in w.
We start counting with 0.
We write w |= L to denote that L satisfies w.
w |= x iff w[0] = x
w |= L1 /\ L2 iff w |= L1 and w |= L2
w |= L1 \/ L2 iff w |= L1 or w |= L2
w |= ! L iff w |= L does not hold
w |= globally L iff forall i. w^i |= L
w |= eventually L iff exists i. w^i |= L
w |= L1 until L2 iff exists i>=0. w^i |= L2 and forall 0<= k < i. w^k |= L1
so either L2 holds immediately, or
at some point in the future, where L1 holds at each instant till that point
w |= next L iff w^1 |= L
Model checking
Check if a model meets a specification.
For our case. Check that the CFSM meets some TCTL or LTL property, written CFSM |= TCTL.
Further reading about model checking
Model checking applications
Verification of hardware/software systems.
Classical uses cases
Get an idea about the "system's" behavior at an early stage.
Validate customer requirements. What do you want? Is this the intended behavior?
We sometimes can automatically generated (runnable) code out of a model. Assuming the model has been validated and the generated code reflects the behavior of the model, the code is verified by construction!
In general, the model is an abstraction of the actual system (some details are left out).
Modern uses
Test case generation.
Build a model of the system.
Either manually (via simulation) or automatically via temporal properties, generate test cases
Issues
Model checking is meant to complete testing and simulation (not a substitute!)
Model checking a Java program directly is not feasible in general.
The model we abstract away certain details (to remain decidable). For example, both branches ("then" and "else") are possible regardless of the Boolean condition.
Hence, model checking highly depends on how accurately the model abstracts the actual system behavior.
Failure in the model does not necessarily mean the behavior can be replayed in the actual system. This is known as "false positives".
On the other hand, an actual bug may be undetected because the model does not fully capture the entire system.
Model checking algorithm
Here's a rough sketch of the model checking algorithm.
CFSM |= TCTL means that all behavior (paths) in the CFSM are also valid in the TCTL formula.
Logically, this corresponds to an implication: forall path. path in CFSM implies path in TCTL.
The standard approach is to check the opposite (contradiction).
exists path. path in CFSM and path not in TCTL.
This property is checked as follows.
Turn the TCTL formula into an automata A1.
Build the complement of A1 which yields automata A2.
Run both, CFSM and A2, simultaneously, if we reach a "final" state in the product automta of A1 and A2, we have found a counter-example!
Otherwise, the property CFSM |= TCTL holds.
References
Software Model Checking Takes Off
A Case Study of Toyota Unintended Acceleration and Software Safety
Hardware model checking (tutorial)
Spin - a popular model checker
UPPAAL
UPPAAL is a modelchecker with a graphical language for modeling based on Communicating Finite State Machines (CFSM) and a temporal specification language based on the Temporal Computation Tree Logic (TCTL). Modelchecking means that UPPAAL verifies if the model satisfies the specification.
From UPPAAL to Go
Let's consider the "coffeemachine" example (see sample solution ilias).
First try
const (
Active = 0
Initial = 1
HasCoffee = 2
)
func coffeeMachine(coffee, enter, exit, payback,
insert20, insert50, insert100 (chan int)) {
var state int = Initial
var acc int = 0
for {
switch {
case state == Initial:
select {
case <-enter:
state = Active
case <-exit:
} // select
case state == Active:
select {
case <-coffee:
if acc >= 150 {
acc = acc - 150
}
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-payback:
if acc > 0 {
acc = 0
}
case <-exit:
state = Initial
} // select
} // switch
} // for
}
There's a problem.
In the UPPAAL model:
- If
acc >= 150 and we synchronize via the coffee channel ...
In our Go implementation,
So, we need to check both conditions (can we synchroinze and is the guard satisfied) atomically! How to do achieve this in Go?
Second try (using default)
Recall the principle of select paired with default.
select {
case ch <- 1: // Action1
default: // Action2
}
With out default, the select will block if we can send via channel ch. With default, we first check all cases, if none of the cases (such as send via channel ch) is available, we pick the default case.
Applied to our example.
Check for guard.
Then, check if synchronization is possible.
If we can't synchronize then "exit" via default.
func coffeeMachine(coffee, enter, exit, payback,
insert20, insert50, insert100 (chan int)) {
var state int = Initial
var acc int = 0
for {
switch {
case state == Initial:
select {
case <-enter:
state = Active
case <-exit:
} // select
case state == Active:
select {
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-exit:
state = Initial
default:
if acc >= 150 {
select {
case <-coffee:
acc = acc - 150
case <-payback:
acc = 0
default:
}
} // if
if acc < 150 && acc > 0 {
select {
case <-payback:
acc = 0
default:
}
}
} // select
} // switch
} // for
}
This works! But is a bit ugly cause we encounter a "busy-waiting loop". We might repeatedly check for the guard and then the synchronization.
Unfortunately, in Go we can't impose a guard condition on the cases in a select statement.
Final try
Idea: Duplicate states by distinguishing if the guard is satisfied or not.
So, in the state state == Active && acc >= 150 a synchronization via coffee is possible.
Here's the implementation of this idea.
func coffeeMachine(coffee, enter, exit, payback,
insert20, insert50, insert100 (chan int)) {
var state int = Initial
var acc int = 0
for {
switch {
case state == Initial:
select {
case <-enter:
state = Active
case <-exit:
} // select
case state == Active && acc >= 150:
select {
case <-coffee:
acc = acc - 150
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-payback:
acc = 0
case <-exit:
state = Initial
} // select
case state == Active && 150 > acc && acc > 0:
select {
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-payback:
acc = 0
case <-exit:
state = Initial
} // select
case state == Active && acc <= 0:
select {
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-exit:
state = Initial
} // select
} // switch
} // for
}
Pro: We no longer require a "busy-waiting" loop.
Cons: Codeduplication (because states are combined with guard conditions).
Complete (final try) code with user
// Translating UPPAAL to Go
// Martin Sulzmann
package main
import "fmt"
const (
Active = 0
Initial = 1
HasCoffee = 2
)
func coffeeMachine(coffee, enter, exit, payback,
insert20, insert50, insert100 (chan int)) {
var state int = Initial
var acc int = 0
for {
switch {
case state == Initial:
select {
case <-enter:
state = Active
case <-exit:
} // select
case state == Active && acc >= 150:
select {
case <-coffee:
acc = acc - 150
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-payback:
acc = 0
case <-exit:
state = Initial
} // select
case state == Active && 150 > acc && acc > 0:
select {
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-payback:
acc = 0
case <-exit:
state = Initial
} // select
case state == Active && acc <= 0:
select {
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-exit:
state = Initial
} // select
} // switch
} // for
}
func coffeeMachineWrong(coffee, enter, exit, payback,
insert20, insert50, insert100 (chan int)) {
var state int = Initial
var acc int = 0
for {
switch {
case state == Initial:
select {
case <-enter:
state = Active
case <-exit:
} // select
case state == Active:
select {
case <-coffee:
if acc >= 150 {
acc = acc - 150
}
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-payback:
if acc > 0 {
acc = 0
}
case <-exit:
state = Initial
} // select
} // switch
} // for
}
func coffeeMachineBusyWait(coffee, enter, exit, payback,
insert20, insert50, insert100 (chan int)) {
var state int = Initial
var acc int = 0
for {
switch {
case state == Initial:
select {
case <-enter:
state = Active
case <-exit:
} // select
case state == Active:
select {
case <-insert20:
acc = acc + 20
case <-insert50:
acc = acc + 50
case <-insert100:
acc = acc + 100
case <-exit:
state = Initial
default:
if acc >= 150 {
select {
case <-coffee:
acc = acc - 150
case <-payback:
acc = 0
default:
}
} // if
if acc < 150 && acc > 0 {
select {
case <-payback:
acc = 0
default:
}
}
} // select
} // switch
} // for
}
func user(userID string, coffee, enter, exit, payback,
insert20, insert50, insert100 (chan int)) {
var state int = Initial
for {
switch {
case state == Initial:
select {
case exit <- 1:
// we remain in Initial
case enter <- 1:
state = Active
}
case state == Active:
select {
case exit <- 1:
state = Initial
case payback <- 1:
case coffee <- 1:
state = HasCoffee
case insert20 <- 1:
case insert50 <- 1:
case insert100 <- 1:
}
case state == HasCoffee:
fmt.Printf("%s: I got coffee \n", userID)
state = Active
}
}
}
func main() {
var coffee = make(chan int)
var enter = make(chan int)
var exit = make(chan int)
var payback = make(chan int)
var insert20 = make(chan int)
var insert50 = make(chan int)
var insert100 = make(chan int)
fmt.Print("Let's get coffee \n")
go coffeeMachine(coffee, enter, exit, payback,
insert20, insert50, insert100)
go user("Max", coffee, enter, exit, payback,
insert20, insert50, insert100)
user("Moritz", coffee, enter, exit, payback,
insert20, insert50, insert100)
}
Static versus dynamic verification
Verification by example
Consider the program.
int f(int n) {
if(n == 0)
return 1;
if(n > 0)
return f(n-1);
if(n < -2)
return f(n+1);
return f(n-1);
}
We observe.
f(5) => f(4) => f(3) => f(2) => f(1) => f(0) => terminates
f(10) => ... => f(0) => terminates
f(-4) => f(-3) => f(-4) => f(-3) => ....
does not seem to terminate (maybe we need to wait a bit longer?)
We verify. For all positive inputs, the function terminates. For example, via an inductive proof.
Dynamic verification
At run-time, execute the program.
Observe its (actual) behavior.
Also commonly referred to as run-time verification and testing.
Static verification
Build approximation of the program's behaviour
Verify that the approximation satisfies some properties.
To remain decidable, we generally need to over-approximate.
Selection of verification methods
Static program analysis
Data-flow analysis
Control-flow analysis
Type and effect systems
Modelchecking
Dynamic program analysis
Testing:
Unit-Tests
Invariants/Assertions
Oracel-based testing
Run-time verification:
This is just a selection
Issues (static verification)
False positives
To carry out the static verification, we need to capture the program's behavior via some appropriate model (e.g. UPPAAL is a good candidate model for Go programs).
In the model we typically neglect certain details so that the static verification task becomes feasible (decidable). We say that the model overapproximates the program's behavior.
Here's an example. Consider the program (sketch).
... // S1
if(cond) {
... // S2
}
else {
... // S3
}
We add comments to label program points.
In the UPPAAL we could keep track of boolean conditions such as cond. However, the model and the verification task becomes then rather involved and potentially no longer decidable. Keep in mind that in cond we can make use of arbitrary Go functions (some may not terminate!).
Hence, we typically build an approximation (abstraction) where we ignore certain details. As the model shall be a faithful representation of the program, we simply assume that both branches of the conditional statement are applicable.
Here's the resulting model.
S1 ---> S2
S2 ---> S3
We make use of labels to represents states. As can be seen, the model is non-deterministic. We can either go from S1 to S2 or S3.
A consequence of this (over)approximation is that we may encounter false positives:
- The static verifier reports failure.
- The failure is observable in the model but NOT in the program.
Recall the above example where we make the conditional statement concrete.
... // S1
if(true) {
... // S2
}
else {
... // S3
}
The else branch is never taken because the Boolean condition always evaluates to true. However, in the transformation from the program to the model, we don't inspect Boolean conditions in detail. We assume that both Boolean results, true and false, are possible. Hence, we obtain the following model.
S1 ---> S2
S2 ---> S3
Suppose there's some verification failure due to state S3. This failure is not reproducible in the program because the else branch is never taken. We encounter a false positive.
False negatives
In the above, we assume that the model overapproximates the program's behavior. That is, the model captures all behavior in the program but possibly more. It could happen that we make a mistake (in the transformation from program to model).
Consider our running example.
... // S1
if(cond) {
... // S2
}
else {
... // S3
}
Suppose we use the following model for verification.
S1 ---> S2
The model is faulty because we igore that from program state S1 we can reach program state S3. Suppose there's a bug once we reach program state S3. This bug doesn't show up in the model. Hence, the verifier reports no failure whereas the program is faulty. We encounter a false negative:
- The static verifier reports okay.
- But the program is buggy.
- The bug is missed because the model transformation is faulty.
Further examples for static verification
Type checking
Types represent a (static) model of the program's run-time behavior. Typically, false positives arise but not false negatives.
lint/FindBugs
These tools look for suspicious program parts by using syntax checks. False positives as well as false negatives may arise.
Dynamic verification
We consider
dynamic verification = testing = run-time verification
Different words with the same intention. Observe the actual program's behavior for a fixed number of program runs. For these fixed number of program runs we try to identify if there is a bug or not.
Unit-Tests
Pros:
- Easy to understand and write
Cons:
- Manual effort. Need to stimulate SUT (=System under Test) via suitable inputs and specify the expected output (result).
Invariants/Assertions
Assertions impose conditions on program locations.
assert(x > 0)
Invariants include more complex properties that not only involves program locations but also functions.
forall x. switchLowHigh(switchLowHigh(x)) == x
Assertions typically make use of Boolean conditions whereas invariants involve more complex (predicate logic) statements.
Oracle-based testing
Oracle = able to predict expected output for any input.
Where does the oracle come from?
- Independent implementation
- Stable release
- ...
Trace-Based Runtime Verification (RV)
Special instance where we are interested in the sequence of events (=trace) emitted by a program.
Monitoring of the runtime behavior of programs to ensure that a given correctness property is satisfied.
Instrumentation of a program to monitor the runtime behavior we are interested in.
Recording of runtime behavior as a sequence of events (= program trace).
Checking that the program trace satisfies the correctness property (= trace validation).
Difference to Modelchecking (MC)
For example, consider the UPPAAL modelchecker and the examples from the Autonomous Systems course. A typical MC example is to guarantee that the user eventually obtains a coffee.
In RV we can only check safety properties ("something bad will never happen") whereas MC typically can also deal with liveness properties ("something good will eventually happen").
RV Topics
Program instrumentation:
Efficiency. As little overhead as possible (time and space). Also important to monitor the 'true' runtime behavior of programs (e.g. consider concurrent programs).
Either online or offline (store trace in a log file for example).
Compiler extension versus domain-specific embedding.
Trace validation:
Pattern formalisms to specify correctness (safety) properties, e.g. regular expressions, LTL, ...
Efficient algorithms to implement pattern formalisms which work under the offline as well as online monitoring assumption.
Explanation of results (beyond yes/no answers).
Simple tracer in Go
package main
import "fmt"
import "time"
import "strconv"
/*
Simple tracer in Go.
Features:
- Can be used offline and online. We only show offline use case
Issues:
- Tracing may be inaccurate. Tracer order may not correspond to actual program execution.
- How to detect stuck threads? We only record events after the operation is performed.
Limitations:
- Naive run-time monitoring via manual inspection of the trace
More systematic run-time monitirong methods:
Apply regular expressions/LTL to validate trace.
*/
// Events
type Kind int
const (
Snd Kind = 0
Rcv Kind = 1
Write Kind = 2
Read Kind = 3
)
type Event struct {
name string
threadId int
kind Kind
}
func mkEvt(n string, t int, k Kind) Event {
return Event{name: n, threadId: t, kind: k}
}
func showEvt(e Event) string {
var s string
switch {
case e.kind == Snd:
s = "!"
case e.kind == Rcv:
s = "?"
case e.kind == Write:
s = "W"
case e.kind == Read:
s = "R"
}
return (strconv.Itoa(e.threadId) + "#" + e.name + s)
}
// Tracer
var globalCnt int
var logChan chan Event
var doneSignal chan int
func initTrace() {
logChan = make(chan Event)
doneSignal = make(chan int)
globalCnt = 0
}
func incCnt() int {
globalCnt++
return globalCnt
}
func recordEvt(e Event) {
go func() {
logChan <- e
}()
}
func done() {
go func() {
doneSignal <- 1
}()
}
func retrieveEvt() (Event, bool) {
var e Event
var r bool
select {
case e = <-logChan:
r = true
default:
r = false
}
return e, r
}
// Variant: Relies on doneSignal channel.
// Doesn't seem to work very well.
func retrieveEvt2() (Event, bool) {
var e Event
var r bool
select {
case e = <-logChan:
r = true
case <-doneSignal:
r = false
}
return e, r
}
// Examples
func example1() {
initTrace()
ch := make(chan int)
t1 := incCnt()
t2 := incCnt()
t3 := incCnt()
// consumer 1
go func() {
for i := 0; i < 10; i++ {
<-ch
e := mkEvt("ch", t1, Rcv)
recordEvt(e)
}
}()
// consumer 2
go func() {
for i := 0; i < 10; i++ {
<-ch
e := mkEvt("ch", t2, Rcv)
recordEvt(e)
}
}()
// producer 3
go func() {
for i := 0; i < 10; i++ {
ch <- 1
e := mkEvt("ch", t3, Snd)
recordEvt(e)
}
}()
// manual synchronization
// wait till all threads are 'done'
time.Sleep(3 * time.Second)
done()
// offline trace analysis
// simply print trace on screen
for {
e, r := retrieveEvt()
if !r {
break
}
fmt.Printf("\n %s", showEvt(e))
}
}
func main() {
example1()
}
