Container data types are ubiquitous in computer programming, enabling developers to efficiently store and process collections of data with an easy-to-use programming interface. Many programming languages offer a variety of container implementations in their standard libraries based on data structures offering different capabilities and performance characteristics. Choosing the best container for an application is not straightforward, as performance characteristics can change drastically in different scenarios, and real-world performance is not always correlated to theoretical complexity. In this paper, we present Primrose, a language-agnostic tool for selecting the best performing valid container implementation from a set of container data types that satisfy the given properties. Semantic properties allow application developers to specify the expected behaviour of a container as a type refinement, e.g., if the container should only contain unique values (such as a set) or should satisfy the LIFO property of a stack. Semantic properties nicely complement syntactic properties (i.e., traits, interfaces, or type classes), allowing developers to specify a container's programming interface and behaviour without committing to a concrete implementation. Primrose automatically select the set of valid container implementations for which the library specifications, written by the developers of container libraries, satisfies the specified properties. Finally, Primrose ranks the valid library implementations based on their runtime performance. We present our prototype implementation of Primrose that preprocesses annotated Rust code, selecting the best performing container implementation. Primrose is easy to integrate in other programming languages. We encode properties and library specifications into verification conditions in a SMT solver to determine the set of valid container implementations.

翻译：容器数据类型在计算机编程中无处不在，它使开发者能够通过易于使用的编程接口高效地存储和处理数据集合。许多编程语言的标准库基于具有不同功能与性能特征的数据结构，提供了多种容器实现。为应用程序选择最佳容器并非易事，因为在不同场景下性能特征可能发生剧烈变化，且实际性能并不总是与理论复杂度相关。本文提出Primrose——一种与编程语言无关的工具，能够从满足指定属性的一组容器数据类型中，选出性能最佳的合法容器实现。语义属性允许应用程序开发者通过类型精化来指定容器的预期行为，例如容器应仅包含唯一值（如集合），或应满足栈的后进先出（LIFO）属性。语义属性与语法属性（即特质、接口或类型类）完美互补，使开发者能够在不绑定具体实现的情况下指定容器的编程接口与行为。Primrose可自动筛选出容器库开发者编写的库规范满足所指定属性的所有合法容器实现。最终，Primrose根据运行时性能对这些合法库实现进行排序。我们展示了Primrose的原型实现，该实现对标注了注解的Rust代码进行预处理，并选出性能最佳的容器实现。Primrose易于集成到其他编程语言中。我们将属性与库规范编码为SMT求解器中的验证条件，以确定合法容器实现的集合。