Hide metadata

dc.date.accessioned2013-03-12T08:01:37Z
dc.date.available2013-03-12T08:01:37Z
dc.date.issued2011en_US
dc.date.submitted2011-03-29en_US
dc.identifier.urihttp://hdl.handle.net/10852/8845
dc.description.abstractDeadlocks are a common error in programs with lock-based concurrency and are hard to avoid or even to detect. One way for deadlock prevention is to statically analyze the program code to spot sources of potential deadlocks. Often static approaches try to confirm that the lock-taking adheres to a given order, or, better, to infer that such an order exists. Such an order precludes situations of cyclic waiting for each other’s resources, which constitute a deadlock. In contrast, we do not enforce or infer an explicit order on locks. Instead we use a behavioral type and effect system that, in a first stage, checks the behavior of each thread or process against the declared behavior, which captures potential interaction of the thread with the locks. In a second step on a global level, the state space of the behavior is explored to detect potential deadlocks. We define a notion of deadlock-sensitive simulation to prove the soundness of the abstraction inherent in the behavioral description. Soundness of the effect system is proven by subject reduction, formulated such that it captures deadlock-sensitive simulation. To render the state-space finite, we show two further abstractions of the behavior sound, namely restricting the upper bound on re-entrant lock counters, and similarly by abstracting the (in general context-free) behavioral effect into a coarser, tail-recursive description.We prove our analysis sound using a simple, concurrent calculus with re-entrant locks.eng
dc.language.isonoben_US
dc.relation.ispartofResearch report http://urn.nb.no/URN:NBN:no-35645en_US
dc.relation.urihttp://urn.nb.no/URN:NBN:no-35645
dc.titleDeadlock checking by a behavioral effect system for lock handlingen_US
dc.typeResearch reporten_US
dc.date.updated2011-10-20en_US
dc.creator.authorPun, Ka I.en_US
dc.creator.authorSteffen, Martinen_US
dc.creator.authorStolz, Volkeren_US
dc.subject.nsiVDP::420en_US
dc.identifier.urnURN:NBN:no-27521en_US
dc.type.documentForskningsrapporten_US
dc.identifier.duo113895en_US
dc.identifier.bibsys112183476en_US
dc.identifier.fulltextFulltext https://www.duo.uio.no/bitstream/handle/10852/8845/1/ResRep-404.pdf


Files in this item

Appears in the following Collection

Hide metadata