Runtime Refinement Checking of Concurrent Data Structures - Department of Information Technology

Questions

Question 1: Let Tid = {t1, t2, t3}, V = {v1, v2, v3}, Actions = {call, return, a1, a2, a3} and the set of public method names be {name1, name2, name3}, give an example of a run r such that r is well-formed.
(Update: the intention of the question is that the reader understands the definition of well-formedness and can give an intuition how a well-formed run looks like with several threads and actions, including call and return. The details of variable assigments and returned lists are optional, but not necessary. )

Question 2: Why does the runtime verification of I/O refinement needs to be improved even with commit acitons added?

Martin

Q1:
This should be a well-formed run:
r = [
s0 = {v1 = 0; v2 = 0; v3 = 0},
a1 = (t1, Call, name1, [1]),
s1 = {v1 = 0; v2 = 0; v3 = 0},
a2 = (t2, Call, name2, [1]),
s2 = {v1 = 0; v2 = 0; v3 = 0},
a3 = (t1, Return, name1, [2]),
s3 = {v1 = 2; v2 = 0; v3 = 0},
a4 = (t3, Call, name3, [4]),
s4 = {v1 = 2; v2 = 1; v3 = 0},
a5 = (t2, Return, name2, [3]),
s5 = {v1 = 2; v2 = 1; v3 = 3},
a6 = (t3, Return, name3, [4]),
s6 = {v1 = 2; v2 = 1; v3 = 3} ]

The lack of connection between arguments, return values, and variable assignments seems to be valid. I let name1 and name2 assign variables on Return, and name3 in the Call action. I believe that to be valid too..?

Q2:
Because the application might not trigger actions that creates traces interesting enough for finding any bugs.

Magnus

Q1:
V={v1,v2,v3}, s0: V={0,0,0}

r = [
(t2,Call,name2,[2,7])
(t3,Call,name3,[3])
a1 -> s1: V={0,7,0}
(t2,Return,name2,[1])
a2 -> s2: V={0,7,3}
(t1,Call,name1,[3])
(t3,Return,name3,[3])
a3 -> s3: V={10,7,3}
(t1,Return,name1,[10])]

Q2:
In some cases, in order to) do meaningful checking of I/O, we would need to add operations that would alter the concurrency characteristics of the application. If we instead capture the behaviour of the implementation of the datastructure as observed from the application that uses it (by means of a _viewer_) then we don't have to modify the I/O code.

Kjell

Q1:
s0 = {v1=0,v2=0,v3=0}
a1 = (t1, Call, name1)
s1 = {v1=0,v2=0,v3=0}
a2 = (t1, a1, name1)
s2 = {v1=1,v2=0,v3=0}
a3 = (t2, Call, name2)
s3 = {v1=1,v2=0,v3=0}
a4 = (t2, a2, name2)
s4 = {v1=1,v2=1,v3=0}
a5 = (t2, Return, name2)
s5 = {v1=1,v2=1,v3=0}
a6 = (t1, Return, name1)
s6 = {v1=1,v2=1,v3=0}

r = s0--a1-->s1--a2--> ... s5--a6-->s6

Q2:
Because some bugs will only be found when particular methods are executed in a particular order. To find more bugs a view of the data structure state can be recorded in the log at every commit point. Erroneous views in the log can be detected and reported to the user even if no method call returns erroneous data.

Stavros

Q1:
{t1, a1, [...]}
{t2, Call, name1, [...]}
{t1, Call, name1, [...]}
{t3, a2, [...]}
{t2, Return, name1, [...]}
{t1, Return, name1, [...]}
{t3, Call, name2, [...]}
{t1, Call, name2, [...]}
{t1, Return, name2, [...]}
{t3, Return, name2, [...]}

Q2:
The runtime verification is based on detecting a particular execution that cannot be mapped back to the specification. If the runtime system does not schedule such an execution (e.g. due to particularly unbalanced usage of interface methods in a particular test), then no errors will be detected.