Modus: A Datalog Dialect for Building Container Images
Containers help share and deploy software by packaging it with all its dependencies. Tools, like Docker or Kubernetes, spawn containers from images as specified by a build system’s language, such as Dockerfile. A build system takes many parameters to build an image, including OS and application versions. These build parameters can interact: setting one can restrict another. Dockerfile lacks support for reifying and constraining these interactions, thus forcing developers to write a build script per workflow. As a result, developers have resorted to creating ad-hoc solutions such as templates or domain-specific frameworks that harm performance and complicate maintenance because they are verbose and mix languages.
To address this problem, we introduce Modus, a Datalog dialect for building
container images. Modus' key insight is that container definitions naturally map to proof trees of Horn clauses. In these trees, container configurations correspond to logical facts, build instructions correspond to logic rules, and the build tree is computed as the minimal proof of the Datalog query specifying the target image. Modus relies on Datalog’s expressivity to specify complex workflows with concision and facilitate automatic parallelisation.
We evaluated Modus by porting build systems of six popular Docker Hub images to Modus. Modus reduced the code size by 20.1% compared to the used ad-hoc solutions, while imposing a negligible performance overhead, preserving the original image size and image efficiency. We also provide a detailed analysis of porting OpenJDK image build system to Modus.
Tue 15 NovDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
14:00 - 15:30
Formal MethodsResearch Papers / Demonstrations at SRC LT 50
Chair(s): Dirk Beyer LMU Munich
Dominic Steinhöfel CISPA Helmholtz Center for Information Security, Andreas Zeller CISPA Helmholtz Center for Information SecurityDOI Pre-print
|Modus: A Datalog Dialect for Building Container Images|
Chris Tomy University College London, Tingmao Wang University College London, Earl T. Barr University College London, Sergey Mechtaev University College LondonDOI
|Multi-Phase Invariant Synthesis|
Daniel Riley Florida State University, Grigory Fedyukovich Florida State UniversityDOI
|Parasol: Efficient Parallel Synthesis of Large Model Spaces|
Clay Stevens University of Nebraska-Lincoln, Hamid Bagheri University of Nebraska-LincolnDOI
|Neural Termination Analysis|
Mirco Giacobbe University of Birmingham, Daniel Kroening University of Oxford, Julian Parsert University of OxfordDOI
|SolSEE: A Source-Level Symbolic Execution Engine for Solidity|
Shang-Wei Lin Nanyang Technological University, Palina Tolmach Nanyang Technological University, Singapore, Institute of High Performance Computing, Agency for Science, Technology and Research (A*STAR), Singapore, Ye Liu , Yi Li Nanyang Technological UniversityPre-print
|MpBP: Verifying Robustness of Neural Networks with Multi-Path Bound Propagation|
Ye Zheng Shenzhen University, Shenzhen, China, Jiaxiang Liu Shenzhen University, Xiaomu Shi Shenzhen University