  We present Locksynth, a tool that automatically derives synchronization
needed for destructive updates to concurrent data structures that involve a
constant number of shared heap memory write operations. Locksynth serves as the
implementation of our prior work on deriving abstract synchronization code.
Designing concurrent data structures involves inferring correct synchronization
code starting with a prior understanding of the sequential data structure's
operations. Further, an understanding of shared memory model and the
synchronization primitives is also required. The reasoning involved
transforming a sequential data structure into its concurrent version can be
performed using Answer Set Programming and we mechanized our approach in
previous work. The reasoning involves deduction and abduction that can be
succinctly modeled in ASP. We assume that the abstract sequential code of the
data structure's operations is provided, alongside axioms that describe
concurrent behavior. This information is used to automatically derive
concurrent code for that data structure, such as dictionary operations for
linked lists and binary search trees that involve a constant number of
destructive update operations. We also are able to infer the correct set of
locks (but not code synthesis) for external height-balanced binary search trees
that involve left/right tree rotations. Locksynth performs the analyses
required to infer correct sets of locks and as a final step, also derives the
C++ synchronization code for the synthesized data structures. We also provide a
performance analysis of the C++ code synthesized by Locksynth with the
hand-crafted versions available from the Synchrobench microbenchmark suite. To
the best of our knowledge, our tool is the first to employ ASP as a backend
reasoner to perform concurrent data structure synthesis.
