Skip to content

Commit

Permalink
Merge pull request #257 from paulgazz/parallelize_kismet
Browse files Browse the repository at this point in the history
This parallelizes kismet, the unmet dependency checker for Kconfig.  kismet works by creating verification conditions for each Kconfig selector and selectee, then uses z3 to check whether the condition allows for an unmet dependency.  The checks for each selector/selectee pair are independent, so they can run in parallel.  There are three checkers, syntactic, optimized, and precise.  Syntactic is so fast, that parallelizing is negligible compared to the other phases.  The optimized and precise checkers have been parallelized.

Previously, the checker code ran a big loop over all pairs of selectors and selectees (and a visibility condition, making it a triple loop).  This merge factors out the code to check each triple and uses python's multiprocessing library to parallelize the checks.  The code has been refactored to make serializing the results possible, to remove some debugging output, to replace progress reporting with tqdm, and to remove an option (--explore-whole-unmet-space) that passed complex, hard-to-serialize state but wasn't really being used.

kismet also validates the resulting unmet dependency alarms by generating example config files that are supposed to trigger the unmet dependency.  This step is not parallelized, since it runs Kconfig (via make) on the actual kernel source tree to see if the warning gets triggered.  Since kismet only expects a single source tree, parallelizing this would require multiple copies of the kernel source.  Moreoever, it's only configuring the kernel, which is pretty fast compared to checking, and there haven't been enough alarms to make a huge difference.  The precise checking has taken vast majority of the time, because it requires checking large constraints with z3 for each selector/selectee.

It has been tested against the original serial implementation in two ways:
- The README's example of 5.16 for x86_64.
  
- The [original paper's](https://doi.org/10.1145/3468264.3468578) [experimental data](https://doi.org/10.5281/zenodo.4885001) for Linux 5.4.4 

  ```
  # running the experiment, assuming kismet is already installed.
  wget https://raw.githubusercontent.com/paulgazz/kmax/master/scripts/kismet_evaluation/kismet_experiments_replication.sh
  bash kismet_experiments_replication.sh
  # getting and comparing to the original results
  wget https://zenodo.org/records/4563310/files/kismet-raw-results-main.zip
  for i in kismet-raw-results-main/raw_kismet/verbose_summaries/kismet_summary_*.txt; do name=$(basename $i); echo diff $i ~/kismet-experiments/$name; done | bash | less
  ```

Fixes #251
  • Loading branch information
paulgazz authored Jul 19, 2024
2 parents 5f44233 + 24d0ed8 commit 063eee3
Show file tree
Hide file tree
Showing 2 changed files with 213 additions and 165 deletions.
Loading

0 comments on commit 063eee3

Please sign in to comment.