Vatras - On the Expressive Power of Languages for Static Variability

[![agda][agda-badge-version-svg]][agda-badge-version-url]

Vatras is the supplementary Agda library for our OOPSLA'24 paper:

On the Expressive Power of Languages for Static Variability. Paul M. Bittner, Alexander Schultheiß, Benjamin Moosherr, Jeffrey M. Young, Leopoldo Teixeira, Eric Walkingshaw, Parisa Ataei, Thomas Thüm. Object-Oriented Programming, Systems, Languages & Applications, 2024 (OOPSLA 2024).

This library formalizes all results in our paper:

All formal languages for static software variability presented in our survey (Section 3 + Table 1) are formalized as algebraic datatypes.
The library implements our formal framework for language comparisons, including necessary data structures, theorems, and proofs (Section 4).
This library contains all theorems and proofs to establish the map of variability languages we find by comparing the languages from our survey with our framework (Section 5).

Additionally, our library comes with a small demo, and tutorials for getting to know the library and for formalizing your own variability languages (see "Tutorials" section below). When run in a terminal, our demo will show a translation roundtrip, showcasing the circle of compilers developed for identifying the map of variability languages (Section 5).

What is Static Variability and What is Vatras?

Vatras is a library to study and compare meta-languages for specifying variability in source code and data. Some software systems are configurable before they are compiled, i.e., statically. A common way to implement static variability is by conditional compilation, as for example possible with the C preprocessor. For instance, the following code snippet from the Linux kernel

#ifdef CONFIG_DEBUG_LOCK_ALLOC
extern bool console_srcu_read_lock_is_held(void);
#else
static inline bool console_srcu_read_lock_is_held(void)
{
  return 1;
}
#endif

replaces the function console_srcu_read_lock_is_held with a default implementation in case a particular feature should be debugged. Essentially, the code snippet above does not denote a single C program but two C programs, each using one of two alternatives for the function console_srcu_read_lock_is_held.

To model and analyze static variability, researchers have formalized various formal languages, including formalisms for conditional compilation. For example, the choice calculus is a small language to formalize conditional compilation in terms of a singly syntactic term, referred to as a choice. A choice F ⟨ l , r ⟩ specifies two alternatives l and r for a feature or configuration option F. Encoding the example above in choice calculus yields

CONFIG_DEBUG_LOCK_ALLOC ⟨ 
  extern bool console_srcu_read_lock_is_held(void);
,
  static inline bool console_srcu_read_lock_is_held(void)
  {
    return 1;
  }
⟩

Apart from source code, static configuration processes emerge in many other areas, including our daily lives. For instance, some restaurants offer your to configure your meal. Sticking to the choice calculus, we may for example specify a configurable sandwich that always has bread 🍞 and cheese, maybe has salad 🥗 (expressed as a choice between Salad 🥗 and an empty value ε), either has a meat 🍖 or falafel 🧆 patty, and has any combination of mayonnaise 🥚 and ketchup 🍅 as follows:

🍞-< 
  Salad⟨ 🥗, ε ⟩,
  🧀,
  Patty⟨ 🍖, 🧆 ⟩,
  Sauce⟨ ε, 🥚, 🍅, 🍅🥚 ⟩
  >-

where the Y-brackets of the outer expression 🍞-< ... >- denote that the ingredients go within the bread (i.e., we build a tree where the ingredients are sub-expressions of bread).

The goal of Vatras is to formalize and compare languages for static variabilty. To this end, we formalize the syntax and semantics of the choice calculus, some of its dialects, and many more formal languages for static variability. For instance, writing out the above sandwich expression in our Agda formalization of the choice calculus, closely resembles the original expressions (most boilerplate comes from explicit list syntax):

sandwich : CCC Feature ∞ Artifact
sandwich =
  "🍞" -<
       "Salad" ⟨ leaf "🥗" ∷ leaf "ε" ∷ [] ⟩
    ∷  leaf "🧀"
    ∷  "Patty" ⟨ leaf "🍖" ∷ leaf "🧆" ∷ [] ⟩
    ∷  "Sauce" ⟨ leaf "ε"  ∷ leaf "🥚" ∷ leaf "🍅" ∷ leaf "🍅🥚" ∷ [] ⟩
    ∷ []
  >-
  where
    leaf : String → CCC Feature ∞ Artifact
    leaf a = a -< [] >-

We may configure our sandwich in terms of the semantics ⟦_⟧ for choice calculus. The semantics is a function takes a configuration as input to produce a variant. For our sandwich example, a configuration decides for each configuration option Salad, Patty, and Sauce which alternative to pick. A variant is a sandwich without any conditional elements left (i.e., a term without choices). From a configuration, we can derive the respective sandwich variant, and we can use Agda to prove that the semantics derive the variant we expect:

config : Feature → ℕ
config "Salad" = 0
config "Patty" = 1
config "Sauce" = 2
config _ = 0

config-makes-falafel-ketchup-sandwich :
  ⟦ sandwich ⟧ config ≡
    "🍞" -<
         leaf "🥗"
      ∷  leaf "🧀"
      ∷  leaf "🧆"
      ∷  leaf "🍅"
      ∷ []
    >-
config-makes-falafel-ketchup-sandwich = refl

Vatras enables semantic comparisons of variability languages based on a meta-theory centered around the three fundamental yet unexplored properties of completeness, soundness, and expressiveness. Completeness serves as a lower bound (i.e., a language can express at least a given semantic domain), soundness serves as an upper bound (i.e., a language can express at most a given semantic domain), and expressiveness serves as a relative comparison (i.e., a language can express at least the semantic domain of another language). Proofs of these properties come as encodings for completeness (i.e., a function that creates a variational expression from a set of variants), enumerations for soundness (i.e., a function that enumerates all variants denoted by a variational expression), and compilers between languages for expressiveness. Vatras includes a range of proofs of these properties for existing languages as explained in our respective paper. As a showcase, Vatras will show a roundtrip translation of the configurable sandwich specification above when you run it. Details on the features implemented in Vatras, including tutorials for integrating new languages, can be found in the Reusability Guide below.

Kick-the-Tires

This section gives you a short "Getting Started" guide. For detailed instructions on setting up dependencies, see the next section. We tested our setup on Manjaro, NixOS, Windows Subsystem for Linux (WSL2), and we also tested the Docker setup on Windows 11 and macOS Ventura 13.0.1 (22A400) on an Apple M1 Pro.

In case of problems, there is a "Troubleshooting" section at the bottom of this file.

Setup

Clone the library to a directory of your choice:

git clone https://github.com/VariantSync/Vatras.git

There are three alternative ways to compile the library and run its small demo. Either use Nix, Docker, or install Agda manually. In general, we recommend Nix because it creates a sandbox environment with all dependencies satisfied while not affecting your system setup (as does Docker), as well as giving you the opportunity to adapt and reuse the library in your own Agda projects (Docker requires to rebuild an image after every change).

For Windows users, we recommend Docker. If you are familiar with Windows Subsystem for Linux (WSL2), you may safely use the other alternatives in WSL2, too. To install WSL2, follow the official instructions.
For Mac users, we recommend Nix or Docker. (We experienced problems with installing Agda manually.)
For Linux users, any alternative is fine but we recommend Nix for the reasons mentioned above.

There are no other software requirements apart from having either Nix, Docker, or Agda installed, depending on which alternative you choose. The only dependency of our library is the Agda standard library which is automatically taken care of by our Nix and Docker setups.

Note that building for the first time (or

Vatras

Install / Use

README

Vatras - On the Expressive Power of Languages for Static Variability

What is Static Variability and What is Vatras?

Kick-the-Tires

Setup