Search for: All records

The Linux kernel is highly-configurable, with a build system that takes a configuration file as input and automatically tailors the source code accordingly. Configurability, however, complicates testing, because different configuration options lead to the inclusion of different code fragments. With thousands of patches received per month, Linux kernel maintainers employ extensive automated continuous integration testing. To attempt patch coverage, i.e., taking all changed lines into account, current approaches either use configuration files that maximize total statement coverage or use multiple randomly-generated configuration files, both of which incur high build times without guaranteeing patch coverage. To achieve patch coverage without exploding build times, we propose krepair, which automatically repairs configuration files that are fast-building but have poor patch coverage to achieve high patch coverage with little effect on build times. krepair works by discovering a small set of changes to a configuration file that will ensure patch coverage, preserving most of the original configuration file's settings. Our evaluation shows that, when applied to configuration files with poor patch coverage on a statistically-significant sample of recent Linux kernel patches, krepair achieves nearly complete patch coverage, 98.5% on average, while changing less than 1.53% of the original default configuration file in 99% of patches, which keeps build times 10.5x faster than maximal configuration files. 

Artifact from "Maximizing Patch Coverage for Testing of Highly-Configurable Software without Exploding Build Times" 

This is the artifact abstract for the ICSE 2024 paper, *Semantic Analysis of Macro Usage for Portability*. This artifact provides the source code of Maki, the tool described in the paper, and instructions on how to run Maki to replicate the results originally reported in the paper. The paper's original results are also included so that one may cross-reference them against the results they obtain while attempting to replicate them. We claim the **available** and **reusable** badges. We believe this artifact deserves the available badge because it is publicly available on Zenodo at https://doi.org/10.5281/zenodo.7783131 (DOI 10.5281/zenodo.7783131). We believe this artifact deserves the reusable badge because it includes instructions for reproducing all the paper's major results, along with a dataset one may verify them against. This artifact also utilizes Docker to facilitate reuse, as recommended in the ICSE 2024 Call for Artifact Submissions. A reviewer who wishes to evaluate this artifact must be familiar with Docker and the Linux command line. Clang and Python experience is advised, but not essential. A reviewer will need Docker to run the artifact, and should have a device with at least 8 threads and 8GB of RAM. "Kicking the tires" and replicating a portion of the paper's original results should take about 20 minutes of time and 2GB of storage memory. Replicating the paper's full results would require over two weeks of time and 620GB of storage memory. The artifact does not require any specific operating system or environment to run. 

Experimental Data for "Maximizing Patch Coverage for Testing of Highly-Configurable Software without Exploding Build Times" 

Artifact from "Maximizing Patch Coverage for Testing of Highly-Configurable Software without Exploding Build Times" 

Configurable software makes up most of the software in use today. Configurability, i.e., the ability of software to be customized without additional programming, is pervasive, and due to the criticality of problems caused by misconfiguration, it has been an active topic researched by investigators in multiple, diverse areas. This broad reach of configurability means that much of the literature and latest results are dispersed, and researchers may not be collaborating or be aware of similar problems and solutions in other domains. We argue that this lack of a common ground leads to a missed opportunity for synergy between research domains and the synthesis of efforts to tackle configurability problems. In short, configurability cuts across software as a whole and needs to be treated as a first class programming element. To provide a foundation for addressing these concerns we make suggestions on how to bring the communities together and propose a common model of configurability and a platform, ACCORD, to facilitate collaboration among researchers and practitioners. 

Highly-configurable software underpins much of our computing infrastructure. It enables extensive reuse, but opens the door to broken configuration specifications. The configuration specification language, Kconfig, is designed to prevent invalid configurations of the Linux kernel from being built. However, the astronomical size of the configuration space for Linux makes finding specification bugs difficult by hand or with random testing. In this paper, we introduce a software model checking framework for building Kconfig static analysis tools. We develop a formal semantics of the Kconfig language and implement the semantics in a symbolic evaluator called kclause that models Kconfig behavior as logical formulas. We then design and implement a bug finder, called kismet, that takes kclause models and leverages automated theorem proving to find unmet dependency bugs. kismet is evaluated for its precision, performance, and impact on kernel development for a recent version of Linux, which has over 140,000 lines of Kconfig across 28 architecture-specific specifications. Our evaluation finds 781 bugs (151 when considering sharing among Kconfig specifications) with 100% precision, spending between 37 and 90 minutes for each Kconfig specification, although it misses some bugs due to underapproximation. Compared to random testing, kismet finds substantially more true positive bugs in a fraction of the time. 

Artifact from "Finding Broken Linux Configuration Specifications by Statically Analyzing the Kconfig Language"