Researcher:
Muşlu, Kıvanç

Job Title

Undergraduate Student

First Name

Kıvanç

Last Name

Muşlu

Name Variants

Muşlu, Kıvanç

Search Results

Now showing 1 - 1 of 1

Metadata only
Run-time verification of optimistic concurrency
(Springer, 2010) Qadeer, Shaz; N/A; Department of Computer Engineering; Department of Computer Engineering; Sezgin, Ali; Taşıran, Serdar; Muşlu, Kıvanç; Researcher; Faculty Member; Undergraduate Student; Department of Computer Engineering; N/A; College of Engineering; College of Engineering; N/A; N/A; N/A
Assertion based specifications are not suitable for optimistic concurrency where concurrent operations are performed assuming no conflict among threads and correctness is cast in terms of the absence or presence of conflicts that happen in the future. What is needed is a formalism that allows expressing constraints about the future. In previous work, we introduced tressa claims and incorporated prophecy variables as one such formalism. We investigated static verification of tressa claims and how tressa claims improve reduction proofs. In this paper, we consider tressa claims in the run-time verification of optimistic concurrency implementations. We formalize, via a simple grammar, the annotation of a program with tressa claims. Our method relieves the user from dealing with explicit manipulation of prophecy variables. We demonstrate the use of tressa claims in expressing complex properties with simple syntax. We develop a run-time verification framework which enables the user to evaluate the correctness of tressa claims. To this end, we first describe the algorithms for monitor synthesis which can be used to evaluate the satisfaction of a tressa claim over a given execution. We then describe our tool implementing these algorithms. We report our initial test results.