Giter VIP home page Giter VIP logo

torte's Introduction

torte: feature-model experiments à la carte 🍰

torte is a declarative workbench for reproducible experiments in feature-model analysis research.

Why torte? Take your pick:

  • "Tseitin or not Tseitin?" Evaluator
  • CNF Transformation Workbench
  • KConfig Extractor that Tackles Evolution
  • Towards Reproducible Feature-Model Transformation and Extraction
  • That's an Obviously Reverse-Engineered Tool Name
  • KConfig = 🍰 config ∧ 🍰 = torte ∎

torte can be used to

  • extract feature models from KConfig-based configurable software systems (e.g., the Linux kernel),
  • transform feature models between various formats (e.g., FeatureIDE, UVL, and DIMACS), and
  • analyze feature models with solvers to evaluate the extraction and transformation impact,

all in a fully declarative and reproducible fashion backed by reusable Docker containers. This way, you can

  • draft experiments for selected feature models first, then generalize them to a larger corpus later,
  • execute experiments on a remote machine without having to bother with technical setup,
  • distribute fully-automated reproduction packages when an experiment is ready for publication, and
  • adapt and update existing experiments without needing to resort to clone-and-own practices.

Getting Started: The Quick Way

This one-liner will get you started with the default experiment (Docker required).

curl -s https://ekuiter.github.io/torte/ | sh

Read on if you want to know more details.

Getting Started: In Detail

To run torte, you need:

Experiment files in torte are self-executing - so, you can just create or download an experiment file (e.g., from the experiments directory) and run it.

The following instructions will get you started on a fresh system. By default, each of these instruction sets will install torte into the torte directory. All experiment data will then be stored in the directories input and output in your working directory.

Ubuntu 22.04

# install and set up dependencies
sudo apt-get update
sudo apt-get install -y curl git make uidmap dbus-user-session

# install Docker (see https://docs.docker.com/desktop/install/linux-install/)
curl -fsSL https://get.docker.com | sh
dockerd-rootless-setuptool.sh install

# download and run the default experiment
curl -s https://ekuiter.github.io/torte/ | sh

macOS 14

# install and set up dependencies (this will replace macOS' built-in bash with a newer version)
/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
(echo; echo 'eval "$(/opt/homebrew/bin/brew shellenv)"') >> $HOME/.zprofile
eval "$(/opt/homebrew/bin/brew shellenv)"
brew install bash coreutils gnu-sed grep

# install Docker (see https://docs.docker.com/desktop/install/mac-install/)
curl -o Docker.dmg https://desktop.docker.com/mac/main/arm64/149282/Docker.dmg
sudo hdiutil attach Docker.dmg
sudo /Volumes/Docker/Docker.app/Contents/MacOS/install --accept-license
sudo hdiutil detach /Volumes/Docker
rm Docker.dmg
open /Applications/Docker.app

# download and run the default experiment
curl -s https://ekuiter.github.io/torte/ | sh

Windows 11

# install WSL (see https://learn.microsoft.com/windows/wsl/install)
powershell
wsl --install

# install Docker (see https://docs.docker.com/desktop/install/windows-install/)
Invoke-WebRequest https://desktop.docker.com/win/main/amd64/149282/Docker%20Desktop%20Installer.exe -OutFile Docker.exe
Start-Process Docker.exe -Wait -ArgumentList 'install', '--accept-license'

# install and set up dependencies
wsl
sudo apt-get update
sudo apt-get install -y curl git make

# download and run the default experiment
curl -s https://ekuiter.github.io/torte/ | sh

Above, we run the default experiment, which extracts, transforms, and analyzes the feature model of BusyBox 1.36.0 as a demonstration. To execute another experiment, run curl -s https://ekuiter.github.io/torte/ | sh -s - <experiment> (a list of predefined experiments is available here). You can also write your own experiments by adapting an existing experiment file.

Further Tips

  • As an alternative to the self-extracting installer shown above, you can clone this repository and run experiments with ./torte.sh <experiment-file>.
  • A running experiment can be stopped with Ctrl+C. If this does not respond, try Ctrl+Z, then ./torte.sh stop.
  • Run ./torte.sh help to get further usage information (e.g., running an experiment over SSH and im-/export of Docker containers).
  • Developers are recommended to use ShellCheck to improve code quality.
  • If Docker is running in rootless mode, experiments must not be run as sudo. Otherwise, experiments must be run as sudo.
  • The first execution of torte can take a while (~30 minutes), as several complex Docker containers need to be built. This can be avoided by loading a reproduction package that includes Docker images (built by ./torte.sh export).

Supported Subject Systems

This is a list of all subject systems for which feature-model extraction has been tested and confirmed to work for at least one extraction tool. Other systems or revisions may also be supported. Detailed system-specific information on potential threats to validity is available in the scripts/subjects directory.

System Revisions Notes
axtls 1.0.0 - 2.0.0
buildroot 2009.02 - 2022.05
busybox 1.3.0 - 1.36.0
embtoolkit 1.0.0 - 1.8.0
fiasco 5eed420 (2023-04-18) 2
freetz-ng d57a38e (2023-04-18) 2
linux 2.5.45 - 6.7 3 4 5
toybox 0.4.5 - 0.8.9 6
uclibc-ng 1.0.2 - 1.0.40

Bundled Tools

Extraction, Transformation, and Analysis

The following tools are bundled with torte and can be used in experiments for extracting, transforming, and analyzing feature models. Most tools are not included in this repository, but cloned and built with tool-specific Docker files in the docker directory. The bundled solvers are listed in a separate table below.

For transparency, we document the changes we make to these tools and known limitations. There are also some general known limitations of torte. 7

Tool Version Date Notes
arminbiere/cadiback 2e912fb 2023-07-21
ckaestne/kconfigreader 913bf31 2016-07-01 8 9 10 11 12 13
ekuiter/clausy 6b816a9 2024-01-15
ekuiter/SATGraf 2677015 2023-04-05 14
FeatureIDE/FeatJAR e27aea7 2023-04-11 15 16
FeatureIDE/FeatureIDE 3.9.1 2022-12-06 17 18 16
paulgazz/kmax 4.5.2 2023-12-20 9 10 19 20 13
Z3Prover/z3 4.11.2 2022-09-04 21

Solvers

The following solvers are bundled with torte and can be used in experiments for analyzing feature-model formulas. The bundled solver binaries are available in the docker/solver directory. Solvers are grouped in collections to allow several versions of the same solver to be used.

In addition to the solvers listed below, z3 (already listed above) can be used as a satisfiability and SMT solver.

Collection: emse-2023

These #SAT solvers (available here) were used in the evaluations of several papers:

The #SAT solvers from the collection model-counting-competition-2022 should be preferred for new experiments.

Solver Version Date Notes
countAntom 1.0 2015-05-11 22
d4 ? ?
dSharp ? ? 23
Ganak ? ?
sharpSAT ? ?

Collection: model-counting-competition-2022

These #SAT solvers (available here) were used in the model-counting competition 2022. Not all evaluated solvers are included here, as some solver binaries (i.e., for MTMC and ExactMC) have not been disclosed.

Solver Version Date Notes
c2d ? ?
d4 ? ?
DPMC ? ?
gpmc ? ?
TwG ? ? 24
SharpSAT-TD ? ? 22
SharpSAT-td+Arjun ? ? 22 25

Collection: other

These are miscellaneous solvers from various sources.

Solver Version Date Class Notes
ApproxMC 4.1.9 2023-02-22 Approximate #SAT Solver
backbone_kissat.py - - Backbone Extractor
d4v2 c1f6842 2023-02-15 #SAT Solver, d-DNNF compiler, PMC
kissat_MAB-HyWalk ? ? SAT Solver
SAT4J 2.3.6 2020-12-14 SAT Solver

Collection: sat-competition

A subset of these SAT solvers (binaries copied/compiled from here) were used in the evaluation of the paper Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses (ASE 2022). Each solver is the gold medal winner in the main track (SAT+UNSAT) of the SAT competition in the year encoded in its file name. We were unable to obtain binaries for the winning solvers in 2008 and 2015.

Year Solver Version Date Notes
2002 zchaff ? ?
2003 Forklift ? ?
2004 zchaff ? ?
2005 SatELiteGTI ? ?
2006 MiniSat ? ?
2007 RSat ? ?
2009 precosat ? ?
2010 CryptoMiniSat ? ?
2011 glucose ? ?
2012 glucose ? ?
2013 lingeling-aqw ? ?
2014 lingeling-ayv ? ?
2016 MapleCOMSPS_DRUP ? ?
2017 Maple_LCM_Dist ? ?
2018 MapleLCMDistChronoBT ? ?
2019 MapleLCMDiscChronoBT-DL-v3 ? ?
2020 Kissat-sc2020-sat ? ?
2021 Kissat_MAB ? ?
2022 Kissat_MAB-HyWalk ? ?
2023 sbva_cadical ? ?

Predefined Experiments

This is a list of all predefined experiments in the experiments directory and their purposes. Please create a pull request if you want to publish your own experiment. Experiments starting with draft- are experimental.

Experiment Purpose
busybox-history-full Extraction of all feature models of BusyBox (for every commit that touches the feature model) 26
default "Hello-world" experiment that extracts and transforms a single feature model
feature-model-collection Extraction, transformation, and analysis of several feature-model histories
feature-model-differences Extraction and comparison of all feature models of several feature-model histories
linux-history-releases Extraction, transformation, and analysis of a history of Linux feature models
linux-history-weekly Extraction of a weekly history of Linux feature models
linux-recent-release Extraction and transformation of a recent Linux feature model
tseitin-or-not-tseitin Evaluation for the paper Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses (ASE 2022)

Project History

This project has evolved through several stages and intends to replace them all:

kmax-vm > feature-model-repository-pipeline > tseitin-or-not-tseitin > torte

  • kmax-vm was intended to provide an easy-to-use environment for integrating kmax with PCLocator in a virtual machine using Vagrant/VirtualBox. It is now obsolete due to our Docker integration of kmax.
  • feature-model-repository-pipeline extended kmax-vm and could be used to extract feature models from Kconfig-based software systems with kconfigreader and kmax. The results were stored in the feature-model-repository. Its functionality is completely subsumed by torte and more efficient and reliable due to our Docker integration.
  • tseitin-or-not-tseitin extended the feature-model-repository-pipeline to allow for transformation and analysis of feature models. It was mostly intended as a reproduction package for a single academic paper. Its functionality is almost completely subsumed by torte, which can be used to create reproduction packages for many different experiments.

If you are looking for a curated collection of feature models from various domains, have a look at our feature-model-benchmark.

If you have any feedback, please contact me at [email protected]. New issues, pull requests, or any other kinds of feedback are always welcome.

License

The source code of this project is released under the LGPL v3 license. To ensure reproducibility, we also provide binaries (e.g., for solvers) in this repository. These binaries have been collected or compiled from public sources. Their usage is subject to each binaries' respective license - please contact me if you perceive any licensing issues.

Footnotes

  1. On arm64 systems (e.g., Windows tablets and Apple Silicon Macs), torte builds cross-platform Docker images to ensure that precompiled binaries (e.g., JavaSMT, Z3, and all solvers) function correctly. This may negatively impact performance on some systems (e.g., ARM-based Windows tablets), although recent Macs should not be affected due to Rosetta.

  2. This system does not regularly release tagged revisions, so only a single revision has been tested. 2

  3. Most revisions and architectures of Linux (since the introduction of KConfig) can be extracted successfully. The user-mode architecture um is currently not supported, as it requires setting an additional sub-architecture.

  4. Currently, we do not consider the more recently introduced Kconfig constructs defined in Linux' scripts/Kconfig.include. This affects the extraction of less than 100 features in the kernel's history up to v6.3.

  5. Currently, we use the KConfig parser of Linux 2.6.9 for all revisions of Linux up to Linux 2.6.9, as older versions of the parser cannot be compiled. We suspect that this does not substantially affect the extracted formula.

  6. Feature models for this system are currently likely to be incomplete due to an inaccurate extraction.

  7. Currently, non-Boolean variability (e.g., constraints on numerical features) is only partially supported (e.g., encoded naively into Boolean constraints). It is recommended to check manually whether non-Boolean variability is represented as desired in generated files.

  8. We added the class TransformIntoDIMACS.scala to kconfigreader to decouple the extraction and transformation of feature models, so kconfigreader can also transform feature models extracted with other tools (e.g., kmax).

  9. We majorly revised the native C bindings dumpconf.c (kconfigreader) and kextractor.c (kmax), which are intended to be compiled against a system's Kconfig parser to get accurate feature models. Our improved versions adapt to the KConfig constructs actually used in a system, which is important to extract evolution histories with evolving KConfig parsers. Our changes are generalizations of the original versions of dumpconf.c and kextractor.c and should pose no threat to validity. Specifically, we added support for E_CHOICE (treated as E_LIST), P_IMPLY (treated as P_SELECT, see smba/kconfigreader), and E_NONE, E_LTH, E_LEQ, E_GTH, E_GEQ (ignored). 2

  10. Compiling the native C bindings of kconfigreader and kmax is not possible for all KConfig-based systems (e.g., if the Python-based Kconfiglib parser is used). In that case, you can try to reuse a C binding from an existing system with similar KConfig files; however, this may limit the extracted model's accuracy. 2

  11. The DIMACS files produced by kconfigreader may contain additional variables due to Plaisted-Greenbaum transformation (i.e., satisfiability is preserved, model counts are not). Currently, this behavior is not configurable.

  12. Feature models and formulas produced by kconfigreader have nondeterministic clause order. This does not impact semantics, but it possibly influences the efficiency of solvers.

  13. The formulas produced by kconfigreader and kmax do not explicitly mention unconstrained features (i.e., features that do not occur in any constraints). However, for many analyses that depend on knowing the entire feature set (e.g., simply listing all configurable features or calculating model counts), this is a threat to validity. We do not modify the extracted formulas, to preserve the original output of kconfigreader and kmax. To address this threat, we instead offer the transformation stage transform-into-unconstrained-features, which explicitly computes these features. 2

  14. We forked the original SATGraf tool and migrated it to Gradle. We also added a new feature for exporting the community structure visualization as a JPG file, avoiding the graphical user interface.

  15. FeatJAR is still in an experimental stage and its results should generally be cross-validated with FeatureIDE.

  16. DIMACS files produced by FeatJAR and FeatureIDE do not contain additional variables (i.e., equivalence is preserved). Currently, this behavior is not configurable. 2

  17. We perform all transformations with FeatureIDE from within a FeatJAR instance, which does not affect the results.

  18. Transformations with FeatureIDE into XML and UVL currently only encode a flat feature hierarchy, no feature-modeling notation is reverse-engineered.

  19. We added the script kclause2model.py to kmax to translate kclause's pickle files into the kconfigreader's feature-model format. This file translates Boolean variability correctly, but non-Boolean variability is not supported.

  20. We do not use kmax's kclause_to_dimacs.py script for CNF transformation, as it has had some issues in the past. Instead, we have a separate Docker container for Z3.

  21. The DIMACS files produced by Z3 may contain additional variables due to Tseitin transformation (i.e., satisfiability and model counts are preserved). Currently, this behavior is not configurable.

  22. This solver currently crashes on some or all inputs. 2 3

  23. This version of dSharp is known to produce inaccurate results for some inputs, so use it with caution.

  24. For TwG, two configurations were provided by the model-counting competition (TwG1 and TwG2). As there was no indication as to which configuration was used in the competition, we arbitrarily chose TwG1.

  25. For SharpSAT-td+Arjun, two configurations were provided by the model-counting competition (conf1 and conf2). As only the second configuration actually runs SharpSAT-td, we chose conf2 (conf1 probably implements the approximate counter SharpSAT-td-Arjun+ApproxMC).

  26. As noted by Kröher et al. 2023, the feature model of BusyBox is scattered across its .c source code files in special comments and therefore not trivial to extract. We solve this problem by iterating over all commits to generate all feature models, committing them to a new busybox-models repository, in which each commit represents one version of the feature model.

torte's People

Contributors

ekuiter avatar

Watchers

 avatar  avatar

torte's Issues

Build of kmax image fails

Building the kmax image currently fails. The reason seems to be that Python 3.6 is used, but the dd dependency (resolved to version 0.6.0) requires Python >= 3.11.

Full build log: build-log.txt

Roadmap

The following issues show the general roadmap for the future development of torte.

Bugs

Minor improvements

  • upgrade Z3 to 4.12.1, see Z3Prover/z3#6577
  • test and improve error handling for missing values (NA), e.g., that failed extractions/transformations propagate appropriately to the other stages (or are ignored)
  • combine iterate with run, deduce file fields automatically based on suffix -file
  • add a filter stage (maybe transient) that removes some input files before executing another stage
  • Z3: for DIMACS, some solvers require that "c " lines occur before "p cnf", Z3 does not do that correctly
  • make transformer and analyzer names consistent with each other
  • make names of columns follow a consistent scheme
  • find out license for each committed blob/binary and document in readme
  • remove CONFIG_ prefix from all files to save space
  • treat Killed (due to OOM killer) as a failure

New Features

  • new algorithms:
  • support evaluation beyond the creation of CSV files (e.g., by integrating more tools)
  • separate the binding and model stages of the extraction (this would require some architectural changes to be able to combine the input directory with the bindings' output directory, but it would make the additional dependencies make and binutils for KConfigReader unnecessary)
  • parallelize extraction
  • auto-calculate the worst possible duration of each stage by taking timeouts into account and estimating evaluation runtime
  • megamodel by introducing an arch choice or applying neg-kc-CNF
  • revise input system so one stage can take multiple input stages and so that aggregate stages do not need to copy all their inputs (e.g., symlinks instead)
  • create "near-correct" feature models (e.g., in UVL) that already omit dead features and also include all unconstrained features to improve the accuracy of extracted models (or, in DIMACS, add number of unconstrained variables to p cnf ...)
  • integrate ConfigFix (which is the spiritual successor to KConfigReader, can export CNF with make cfoutconfig)

Improving External Validity

  • add more systems (i.e., systematically search GitHub for compatible Kconfig projects, some ideas are listed in the experiment files, e.g., u-boot)
  • add feature-model hierarchies (e.g., act as consumer and supplier to https://github.com/SoftVarE-Group/feature-model-benchmark)
  • add more solvers (e.g., a portfolio solver, more solvers can be found in competitions)
  • reproduce ASE'22 evaluation (e.g., add core/dead feature calculation) - currently, at least axTLS and freetz-ng seem buggy
  • for each subject system, determine the best Linux KConfig binding version and possibly update them
  • find a more elegant way to work around the Kconfig helper macros
  • reproduce the results of existing evaluations (e.g., TypeChef) with other CNF transformations and/or KConfig extractors
  • implement SAT format, which is used by some tools as input, as an addition to .model and .smt
  • find a good way to store/upload Docker images and extracted models (really large files, Zenodo? Git LFS? university?)
  • add virtualbox/vagrant image for easier reproduction

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.