Skip to main content
Department of Information Technology

Runtime Refinement Checking of Concurrent Data Structures

Description (Abstract)

We present a runtime technique for checking that a concurrent implementation of a data structure conforms to a high-level executable specification with atomic operations. The technique consists of two phases. In the first phase, the implementation code is instrumented in order to record information about its execution into a log. In the second phase, a verification thread runs concurrently with the implementation and uses the logged information to check that the execution conforms to the high-level specification. We pay special attention to reducing the impact of the runtime analysis on the concurrency characteristics and performance of the implementation. We are currently applying our technique to Boxwood, a distributed implementation of a B-link tree data structure.

Link to the paper


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?


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..?

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


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

r = [
a1 -> s1: V={0,7,0}
a2 -> s2: V={0,7,3}
a3 -> s3: V={10,7,3}

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.


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

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.


{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, [...]}

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.

Updated  2013-06-19 11:45:19 by Stavros Aronis.