Unbounded Thread–Creation in Dynamic Pointer Programs Extended Abstract.pdf

Unbounded Thread–Creation in Dynamic Pointer Programs Thomas Noll and Stefan Rieger RWTH Aachen University Software Modeling and Verification Group 52056 Aachen, Germany {noll,rieger}@cs.rwth-aachen.de Extended Abstract: Techniques for the verification of elementary properties of pointer programs are highly desirable. Programming with pointers is error–prone with potential pit- falls such as dereferencing null pointers and the creation of memory leaks. So far, the field of pointer analysis has focused primarily on sequential programs. But pointer programming becomes even more vulnerable in a concurrent setting where threads can be dynamically created, and where data structures such as linked lists are manipulated and inspected by several threads. We present an approach to model checking of con- current programs that operate on singly–linked lists. var x, y; To the best of our knowledge, it is the first work which proc main( combines unbounded creation of pointer–manipulating 01 new(x); threads with an expressive logic. Moreover existing ap- 02 spawn(server); proaches that support reasoning about dynamic data ) structures make use of non–standard logics, advanced server( model–checking procedures or extended versions of 11 spawn(worker); Hoare logics with accompanying deduction techniques. 12 atc(tt); In contrast, the approach advocated in this paper stays within the realm of traditional (linear–time) model 13 y := x;