Colin S. Gordon, Michael D. Ernst, Dan Grossman. Static Lock Capabilities for
Deadlock Freedom. Technical Report UW-CSE-11-10-01, Computer Science and Engineering,
University of Washington, Seattle, WA, USA. October 2011.
[+abstract]
[+bibtex]
[pdf ]
[dept pdf | dept TRs]
Abstract: We present a technique - lock capabilities - for statically verifying that
multithreaded programs with locks will not deadlock. Most previous work is built around a strict
total order on all locks held simultaneously by a thread, but such an invariant often does not hold
with fine-grained locking, especially when data-structure mutations change the order locks are
acquired. Lock capabilities support idioms that use fine-grained locking, such as mutable binary
trees, circular lists, and arrays where each element has a different lock.
Lock capabilities do not enforce a total order and do not prevent external references to
data-structure nodes. Instead, the technique reasons about static capabilities, where a thread
already holding locks can attempt to acquire another lock only if its capabilities allow it.
Acquiring one lock may grant a capability to acquire further locks, and in data-structures where
heap shape affects safe locking orders, we can use the heap structure to induce the
capability-granting relation. Deadlock-freedom follows from ensuring that the capability-granting
relation is acyclic. Where necessary, we restrict aliasing with a variant of unique references to
allow strong updates to the capability-granting relation, while still allowing other aliases that
are used only to acquire locks while holding no locks.
We formalize our technique as a type-and-effect system, demonstrate it handles realistic challenging
idioms, and use syntactic techniques (type preservation) to show it soundly prevents deadlock.
@techreport{uw-cse-11-10-01,
author = {Colin S. Gordon and Michael D. Ernst and Dan Grossman},
title = {{Static Lock Capabilities for Deadlock Freedom}},
year = 2011,
number = "UW-CSE-11-10-01",
institution={{Computer Science and Engineering, University of Washington}},
address = {{Seattle, WA, USA}},
}
Colin Stebbins Gordon. Type-Safe Stack Traversal for Garbage
Collector Implementation. Brown University Senior Honors Thesis. May 2008.
Undergraduate Thesis.
[+abstract]
[+bibtex]
[pdf]
[slides]
[other
honors theses]
Abstract: Garbage collectors are an important part of many modern
language runtimes. Essentially all tools for developing and
debugging programs using garbage collection assume the
correctness of the collector, and therefore provide no means
for detecting garbage collector errors. As a result it is especially
important that garbage collector implementations be
free of errors. This goal is even more challenging in the face
of the typical implementation strategy for collectors: implementation
in C, making error-prone inferences from complex
bit patterns, where an error could result in dereferencing an
invalid pointer or corrupting program data.
One approach to reducing errors in collector implementation
is to improve both the type-safety and memory-safety
of garbage collector implementations. Prior work in
this direction has focused on the use of modern type systems
to statically detect errors in the collector code at compile
time, but has practical shortcomings. The prior work
replaces the standard machine stack with a heap allocated
data structure to avoid unsafe walks of the native stack.
Traversal of the runtime stack is normally not possible in
higher-level languages because they trade the flexibility of
arbitrary memory access --- typically used to gather a root
set from a runtime stack --- for the safety of being unable to
cause memory access errors.
We present a method for addressing the safe stack traversal
problem at the compiler level, by lifting actual machine
stack frames up to the level of explicit data structures in
Standard ML, such that complete stack traversal can be performed
with minimal unsafe code. We implement a garbage
collector in the ML Kit using the techniques described
and provide details on key parts of the implementation.
@misc{ugradthesis,
author="Colin Stebbins Gordon",
title={{Type-Safe Stack Inspection for Garbage Collector Implementation}},
howpublished={Brown University Senior Honors Thesis},
year=2008,
month="May",
note="Undergraduate Thesis"
}
Meyerovich, L.A., Weinberger, J.H.W., Gordon, C.S.,
Krishnamurthi, S.: ASM Relational Transducer Security Policies. Technical Report
CS-06-12, Computer Science Department, Brown University, Providence, RI, USA.
November, 2006.
[+abstract]
[+bibtex]
[pdf ]
[department
page]
This report is essentially
an extended version of Composition with Consistent Updates for Abstract State
Machines
Abstract: We present a model of the security policy for the Web-based Continue conference
management tool. The policy model and properties are written as ASM Relational
Transducers, which we extend with a module system in order to simplify the
handling of conflicting updates. We assume prior familiarity with the security
policy concerns surrounding Continue. First, we review the ASM Relational
Transducer modeling and property language. Then we describe the basic structure
of our policy implementation and demonstrate the ability to model useful
properties in the original core ASM language. We exploring the use of the
unmodified modeling language in a security policy context and describe typical
ASM Relational Transducer complexity concerns and how these minimally impact our
implementation. Next, we discuss difficulties encountered in representing our
policy and properties in the standard ASM language, including our implementation
in the appendices. Following the description of adapting ASMs for use in
security modeling, we introduce policy modules and a composition operator to
overcome the difficulty of programming in the original language known as the
consistent update problem. Finally, we describe a reduction from our extended
language to the original language, and prove it satisfies our required
correctness property.
@techreport{cs06-12,
author="Leo A. Meyerovich and Joel H. W. Weinberger and
Colin S. Gordon and Shriram Krishnamurthi",
title="{ASM} Relational Transducer Security Policies",
institution="Computer Science Department, Brown University",
year=2006,
number="CS-06-12",
address="Providence, RI, USA"
}