BlockQuickSort Verification with JJBMC

Overview

This project focuses on verifying the correctness of the BlockQuickSort algorithm using JJBMC and JML. The main objectives include:

• Implementing BlockQuickSort in Java.
• Creating JML specifications for modular verification.
• Adapting and extending JJBMC for verification.
• Ensuring the permutation property.
• Evaluating JJBMC's limitations and performance.

The aim is to increase confidence in BlockQuickSort's correctness and explore the potential of JJBMC and JML in software verification.

JJBMC is a tool that is developed both at FZI and KIT, which enables the software bounded model checker JBMC to verify contracts written in the Java Modeling Language (JML).

Building JJBMC

Requirements

• Java 8 (both newer and older versions do not work due to incompatibilities with OpenJML)
• Gradle 6.4.1 or higher (only if gradle wrapper does not work on your system)
• Preferably some Unix OS (tested only on Ubuntu 20.04)

Compiling JJBMC

• Make sure that JAVA_HOME points to a valid installation of Java 8 (tested for openjdk).
• Checkout the source code via git clone git@github.com:JonasKlamroth/JJBMC.git (for a checkout using SSH).
• Build the jar file via ./gradlew fatJar (JJBMC.jar will appear in the root folder of your project).
• If the previous step does not work, first create a gradle wrapper via gradle wrapper.

Running JJBMC

• Important: JJBMC uses JBMC as a backend. Please make sure that a recent version (currently >= 5.22) of JBMC is installed and included in the path. To download and install the latest JBMC version (as part of CBMC) go to https://github.com/diffblue/cbmc/releases/.
• You can see the available command-line options via java -jar JJBMC.jar.
• In general, you can run JJBMC via java -jar JJBMC.jar JAVA_FILE METHOD_NAME -j="JBMC_OPTIONS", where JAVA_FILE should be replaced by the JML-specified Java file that you want to analyze, METHOD_NAME can be replaced by a name of a method you would like to verify (if left out all methods are verified), and JBMC_OPTIONS should be replaced by the JBMC options that you want to set, e.g., a bound for loop unrollings via --unwind BOUND (BOUND should be replaced by the size of the desired bound). For examples, see the section below.

BlockQuickSort Verification

All code relating to the verification of BlockQuickSort can be found in the bqs folder. The following sections describe the different parts of the project.

BlockQuickSort Implementation (bqs/baseCode)

• The original implementation of BlockQuickSort can be found in the bqs/baseCode/BlockQuickSort.hpp folder. The implementation is the one from the original paper.

• A contextual simplified translation of the implementation to Java can be found in bqs/baseCode/BlockQuickSort.java. This translation is used for verification with JJBMC.

• A testing script for the Java implementation can be found in bqs/baseCode/BlockQuickSortTest.java. This script can be used to test the Java implementation against some test cases.

Scripts (bqs/scripts)

The bqs/scripts folder contains scripts that can be used to run JJBMC on the Java implementation of BlockQuickSort. The scripts are described in the following sections.

• bqs/scripts/runner.py is a file for starting JJBMC on the Java implementation of BlockQuickSort. It can be used to run JJBMC on the Java implementation of BlockQuickSort with different parameters. The script can be run with the following command: python3 runner.py It will thereby run multiple instances of JJBMC with sensible bounds for each of the functions defined in BlockQuickSort.

• bqs/scripts/processing.py is a file that processes the output of the runner. It will generate csv files containing information about the runs of the runner and will save them to bqs/processed.

• bqs/scripts/plotting.py is a file to create plots from the csv files generated by the processing script. It will generate plots and save them to bqs/processed.

BlockquickSort Verification (bqs/BlockQuickSort.java)

This file contains the compleatly annotated version of the Java implementation of BlockQuickSort. It is annotated with JML annotations and can be verified with JJBMC.

Publications

My Bachelor's Thesis:

• Bernhard Beckert, Jonas Klamroth, and Bertil Braun: Evaluation of the Bounded Model Checkers JJBMC Based on a Case Study (BlockQuickSort).

Publication introducing BlockQuickSort:

• Stefan Edelkamp and Armin Weiß: BlockQuicksort: How Branch Mispredictions don’t affect Quicksort.

Publication introducing JJBMC:

• Bernhard Beckert, Michael Kirsten, Jonas Klamroth, and Mattias Ulbrich: Modular Verification of JML Contracts Using Bounded Model Checking. (in proceedings of ISOLA 2020)

Publications of research in which JJBMC was used:

• Martin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich, and Alexander Weigl: Formal Specification and Verification of JDK’s Identity Hash Map Implementation (in proceedings of iFM 2022)
• Jonas Klamroth, Florian Lanzinger, Wolfram Pfeifer, and Mattias Ulbrich: The Karlsruhe Java Verification Suite (In The Logic of Software, Springer, 2022)