|
Abstract.
Software systems often use specialized combinations of data structures
to store and retrieve data. Designing and maintaining custom data
structures particularly concurrent ones is time-consuming and
error-prone. We let the user declare the required data as a high-level
specification of a relation and method interface, and automatically
synthesize correct and efficient concurrent data representations. We
present provably sound syntactic derivations to synthesize structures
that efficiently support the interface. We then synthesize
synchronization to support concurrent execution on the structures.
Multiple candidate representations may satisfy the same specification
and we aim at quantitative selection of the most efficient candidate.
Previous works have either used dynamic auto-tuners to execute and
measure the performance of the candidates or used static cost functions
to estimate their performance. However, repeating the execution for
many candidates is time-consuming and a single performance model cannot
be an effective predictor of all workloads across all platforms. We
present a novel approach to quantitative synthesis that learns the
performance model. We developed a synthesis tool called Leqsy that
trains an artificial neural network to statically predict the
performance of candidate representations. Experimental evaluations
demonstrate that Leqsy can synthesize near-optimum representations.
|
|