Skip to content

bblum/landslide

Repository files navigation

landslide

Landslide is a concurrency testing framework for student thread library and kernel projects. It uses systematic testing (also known as stateless model checking) to exhaustively test all thread interleavings possible under a given test program, or failing that, heuristically prioritizes the most promising preemption points to find bugs as quickly as possible should they exist.

If you are a current student please make sure to complete the sign-up form before using Landslide:

The lecture slides associated with this research are available at:

Other reading material:

Guide to this repository:

  • src/bochs-2.6.8.tar.bz2: unmodified distribution of the Bochs simulator
  • src/landslide: Landslide
  • src/patches: Interface code between Landslide and Bochs, including a patch to edit its API slightly, the Makefile, and the module entrypoint.
  • id/: Quicksand (the iterative deepening wrapper described in the OOPSLA paper)
  • *-setup.sh: student-friendly initialization scripts for various class projects
  • pebsim/: directory for running bochs (config files, annotation scripts)
  • pebsim/p2-basecode: directory for importing Pebbles thread library code
  • pebsim/pintos: directory for importing Pintos kernel code

License information

The code in this repository is distributed under mixed licenses according to the following directory structure:

  • Landslide (src/landslide), Quicksand (id/), and all the instrumentation scripts (pebsim/*.sh) are distributed under the 3-clause BSD license (LICENSE).

  • Bochs (src/bochs-2.6.8.tar.bz2) is licensed under the LGPL and distributed in its unmodified tarball. Its license is contained therein.

  • Interface code between Landslide and Bochs (src/patches/) is subject to LGPL.

  • Landslide incorporates the Linux rbtree implementation (src/rbtree) which is licensed under GPLv2.

  • The P2 basecode (pebsim/p2-basecode/p2-*.tar.bz2) is distributed unlicensed with express permission from its copyright holders; please refer to the its LICENSE file in the tarball.

Linking Landslide with Bochs and the rbtree produces a result which is subject to the terms of the GPL to redistribute.

About

stateless model checking for thread libraries, kernels, and transactional memory

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors