Skip to content

Commit

Permalink
Updating the repository for the public version on github.
Browse files Browse the repository at this point in the history 
(squashed commit)
  • Loading branch information
@mattulbrich
mattulbrich committed Oct 27, 2023
1 parent d68fa2c commit 4e58ad5
Show file tree
Hide file tree
Showing 92 changed files with 360,627 additions and 3,214 deletions.
73 changes: 73 additions & 0 deletions .github/dlsmt.sh
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
# No shebang!

## Weigl's little helper to download SMT-solvers.
# SPDX-License-Identifier: GPL-2.0-or-later

# This script is meant to be executed inside an Github Action to download the SMT-solver.
# It uses the Github cli tool "gh", which allows an easy access to the releases of a
# repository, and to download it artifacts.
#
# This script will always the latest uploaded artifact.
#
#
# For performance, you should consider caching. This script skips downloading if files are present.


## Github workflow commands
# Please have a look at https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions
# which explains a lot of workflow commands and special files in Github Actions.


## TODO
# It would be nice to convert it into a real! Github action, which can also exploit
# the API library of Github. A manual/tutorial is here:
#
# https://docs.github.com/en/actions/creating-actions/developing-a-third-party-cli-action

mkdir smt-solvers
cd smt-solvers


#################################################
echo "::group::{install z3}"
echo "Check for Z3, if present skip installation"

if readlink -f */bin/z3; then
echo "::notice::{Z3 found. Caching works! Skip installation}"
else
echo "Download Z3"
wget 'https://github.com/Z3Prover/z3/releases/download/z3-4.12.2/z3-4.12.2-x64-glibc-2.31.zip'
unzip -n z3*.zip
rm z3-*.zip
fi

Z3=$(readlink -f */bin/z3)
chmod u+x $Z3
echo "Z3 added to path: $Z3"
echo $(dirname $Z3) >> $GITHUB_PATH

echo "::endgroup::"
#################################################

#################################################
echo "::group::{install cvc5}"
if -f cvc5-Linux; then
echo "::notice::{Z3 found. Caching works! Skip installation}"
else
echo "Install CVC5"
gh release download --skip-existing -p 'cvc5-Linux' -R cvc5/cvc5
fi

CVC5=$(readlink -f cvc5-Linux)
echo "CVC5 installed and added to path: CVC5"
chmod u+x $CVC5
echo $(dirname $CVC5) >> $GITHUB_PATH

echo "::endgroup::"
#################################################

echo "::group::{check installation/versions}"
$Z3 -version

$CVC5 --version
echo "::endgroup::"
82 changes: 38 additions & 44 deletions .github/workflows/tests.yml
View file
Original file line number Diff line number Diff line change
@@ -1,51 +1,45 @@
name: Broad Release Tests
name: Proof Replay

on:
workflow_dispatch:
push:
branches: ["main", "master"]
schedule:
- cron: '0 5 * * 1' # every monday morning
on: [ push ]

permissions:
checks: write
checks: write

jobs:
unit-tests:
strategy:
fail-fast: false
matrix:
os: [macos-latest, ubuntu-latest, windows-latest]
java: [8,11,17,21]
continue-on-error: false
runs-on: ${{ matrix.os }}
env:
GH_TOKEN: ${{ github.token }}
steps:
- uses: actions/checkout@v3
- name: Set up JDK ${{ matrix.java }}
uses: actions/setup-java@v3
with:
java-version: ${{ matrix.java }}
distribution: 'corretto'
compile_and_test:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Set up JDK 21
uses: actions/setup-java@v3
with:
java-version: 21
distribution: 'corretto'
- name: Build with Gradle
uses: gradle/gradle-build-action@v2.4.2
with:
arguments: --continue assemble check

- name: Build with Gradle
uses: gradle/gradle-build-action@v2.4.2
with:
arguments: --continue test
replay-proofs:
strategy:
fail-fast: false
matrix:
# target: [ check-overflow-methods, check-overflow-constructors, check-methods, check-constructors ]
# Reduce checks until overflow is fixed
target: [ check-methods, check-constructors ]
runs-on: ubuntu-latest
env:
GH_TOKEN: ${{ github.token }}

- name: Verify with KeY
uses: gradle/gradle-build-action@v2.4.2
with:
arguments: --continue checkAll


- name: Upload test results
uses: actions/upload-artifact@v3.1.1
if: success() || failure()
with:
name: test-results-${{ matrix.os }}
path: |
**/build/test-results/*/*.xml
**/build/reports/
!**/jacocoTestReport.xml
steps:
- uses: actions/checkout@v3
- name: Set up JDK 21
uses: actions/setup-java@v3
with:
java-version: 21
distribution: 'corretto'
- name: Install SMT-Solvers
run: .github/dlsmt.sh
shell: bash
- name: "Verify with KeY ${{ matrix.target }}"
run: make ${{ matrix.target }}
50 changes: 50 additions & 0 deletions Makefile
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
KEY_JAR=tools/key-2.11.0-exe.jar
KEY_OVERFLOW_JAR=tools/key-2.11.0-o-exe.jar
CI_TOOL=tools/citool-1.4.0-mini.jar

checkCommand=java -Dlogback.configurationFile=./gradle/disablelogging.xml -Dkey.contractOrder="contract-order.txt" -cp "$(KEY_JAR):$(CI_TOOL)" de.uka.ilkd.key.CheckerKt --no-auto-mode --proof-path src/main/key

checkOverflowCommand=java -Dlogback.configurationFile=./gradle/disablelogging.xml -Dkey.contractOrder="contract-order.txt" -cp "$(KEY_OVERFLOW_JAR):$(CI_TOOL)" de.uka.ilkd.key.CheckerKt -v --no-auto-mode --proof-path src/main/key-overflow

default:
@echo Available targets:
@sed -n 's/^\([a-zA-Z_-]\+\):.*/ \1/p' Makefile

proofSettings:
mkdir -p $${HOME}/.key
cp proofIndependentSettings.props $${HOME}/.key

run:
@echo Consider loading one of the following files:
@find -iname "project*.key"
java -Dkey.contractOrder="contract-order.txt" -jar $(KEY_JAR)

compile:
find -name "*.java" > sources.txt
javac @sources.txt

constr-src:
rm -rf src/main/java-constr
cp -r src/main/java src/main/java-constr
sed -i 's/no_state int bucketStart/int bucketStart/' src/main/java-constr/de/wiesler/BucketPointers.java
sed -i 's/no_state int bucketSize/int bucketSize/' src/main/java-constr/de/wiesler/BucketPointers.java

constr-overflow-src:
rm -rf src/main/java-constr-overflow
cp -r src/main/java src/main/java-constr-overflow
sed -i 's/no_state int bucketStart/int bucketStart/' src/main/java-constr-overflow/de/wiesler/BucketPointers.java
sed -i 's/no_state int bucketSize/int bucketSize/' src/main/java-constr-overflow/de/wiesler/BucketPointers.java

check: check-methods check-constructors check-overflow-methods check-overflow-constructors

check-methods: proofSettings
$(checkCommand) --forbid-contracts-file "contracts/ignore.txt" --forbid-contracts-file "contracts/constructors.txt" -s statistics-methods.json src/main/key/project.key

check-constructors: constr-src
$(checkCommand) --contracts-file contracts/constructors.txt -s statistics-constructors.json src/main/key/project-constr.key

check-overflow-methods:
$(checkOverflowCommand) --contracts-file "contracts/overflow.txt" --forbid-contracts-file "contracts/constructors.txt" -s statistics-overflow-methods.json src/main/key-overflow/project.key

check-overflow-constructors: constr-overflow-src
$(checkOverflowCommand) --contracts-file "contracts/constructors.txt" -s statistics-overflow-constructors.json src/main/key-overflow/project-constr.key
157 changes: 147 additions & 10 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -1,22 +1,159 @@
# Formal Specification and Verification of a Java Implementation of In-Place Super Scalar Sample Sort
# A Formally Verified Efficient Sorting Routine For Java

This is the verified code and all proof files.
This repostiory contains a sorting routine for Java programs that
combines two important properties that a decent algorithm should have: [2]
1. The implementation is competitively efficient.
2. The implementation is correct in all possible application cases.

The code in [`src`](src) is based on [this](https://github.com/jwiesler/ips4o) Rust rewrite of the [original paper implementation](https://github.com/ips4o/ips4o).
The first point is shown empirically by benchmarking (see Section 5 of
[2] and the [Sascha Witt's
repository](https://github.com/SaschaWitt/ips4o-java-benchmark)). The
correctness of the implementation has been formally proven using the
[deductive verification engine KeY](https://www.key-project.org) with
which Java programs can be verified against a formal specification
using the [Java Modeling Language
(JML)](https://www.cs.ucf.edu/~leavens/JML/index.shtml).

The proofs are located in [`proofs`](proofs) and can be loaded using the KeY binaries in [`tools`](tools).
The [`contracts`](contracts) folder contains listing of subsets of all contracts used for filtering.
The proof statistics can be found in [`statistics`](statistics).
You can use the algorithm in your Java programs by declaring a
maven/gradle dependency in your project (s. below).

## In-Place Super Scalar Sample Sort

The sorting algorithm [1] implemented in this project is a Java
implementation of in-place super scalar sample sort (ips4o), an award
winning highly efficient sorting routine that was algorithmically
engineered to make use of CPU features like caching, predictive
execution or SIMD.

The [source code](src/main/java) is based on [this Rust
rewrite](https://github.com/jwiesler/ips4o) of the [original paper
implementation](https://github.com/ips4o/ips4o).

The source code comprises approximately 900 lines of code. The JML
specification that annotates the Java code (in comments) adds another
2500 lines to the sources.

## Using ips4o in your project

You can use the following [maven coordinates](todo) to use `ips4o` in your JVM projects.


```groovy
dependencies {
implementation("org.key-project.ips4o:ips4o-verify:1.0")
}
```

```xml
<dependency>
<groupId>org.key-project.ips4o</groupId>
<artifactId>ips4o-verify</artifactId>
<version>1.0</version>
</dependency>
```

## Verified Properties

In this case study, the following properties of the Java ips4o implementation
have been specified and successfully verified:
1. **Sorting Property:** The array is sorted after the method invocation.
2. **Permutation Property:** The content of the input array after sorting is a permutation of the initial content.
3. **Exception Safety:** No uncaught exceptions are thrown.
4. **Memory Safety:** The implementation does not modify any previously allocated memory location except the entries of the input array.
5. **Termination:** Every method invocation terminates.
6. **Absence of Overflows:** During the execution of the method, no integer operation will overflow or underflow.

The top-level specification of the sorting routine reads as follows:
```
/*@ public normal_behaviour
@ requires values.length <= Buffers.MAX_LEN;
@
@ ensures \dl_seqPerm(\dl_array2seq(values), \old(\dl_array2seq(values)));
@ ensures Functions.isSortedSlice(values, 0, values.length);
@
@ assignable values[*];
@*/
public static void sort(int[] values) { ... }
```

This repository contains the verified code incl. the specification and all proof files.

## Usage
You can either run the respective KeY binaries in [`tools`](tools) or take some inspiration from the [`justfile`](justfile).

Make sure to pass `-Dkey.contractOrder="<path to contract-order.txt>"` to java such that the contract order file is loaded.
### Compilation

In order to compile the sources invoke
```
./gradlew compileJava
```

In order to obtain a jar file with the binary class files of the implementation invoke
```
./gradlew jar
```
and find the jar file in `./build/libs/ips4o-verify-1.0.jar`.

### Verification

In order to check / redo the proofs, you can load the interactive interface of KeY using
```
make run
```

To check whether all proofs can be replpayed, invoke
```
make check
```
This may take some time (possible hours).

You find the respective KeY binaries in the directory
[`tools`](tools). The [`Makefile`](Makefile) gives you hints on how to
execute the checker.

The proofs are located in [`proofs`](proofs) and can be loaded using
the KeY binaries in [`tools`](tools).

The [`contracts`](contracts) folder contains listing of subsets of all
contracts used for filtering. The proof statistics can be found in
[`statistics`](statistics).


Make sure to pass `-Dkey.contractOrder="<path to contract-order.txt>"`
to java such that the contract order file is loaded.

## Caveats
* Overflow proofs and annotations can be found on the branch `overflow`. They have to be loaded using the second KeY binary [`key-2.11.0-o-exe.jar`](tools/key-2.11.0-o-exe.jar).
* To run proofs in [`contracts/constructors.txt`](contracts/constructors.txt) the `no_state` modifier on `BucketPointers::bucketStart` and `BucketPointers::bucketSize` has to be removed. Both methods are only `no_state` when using the final heap which has a soundness problem with constructors. There is currently no nicer way to do this in KeY automatically.

* The overflow proofs have been conducted after the other proofs. The
annotated sources can be found under
[`src/main/java-overflow`](src/main/java-overflow). In them most
artifacts are assumed without proving them (using the `_free`) since
they have been shown in the original proof obligations. They have
to be loaded using the second KeY binary
[`key-2.11.0-o-exe.jar`](tools/key-2.11.0-o-exe.jar).

* To run proofs in
[`contracts/constructors.txt`](contracts/constructors.txt) the
`no_state` modifier on `BucketPointers::bucketStart` and
`BucketPointers::bucketSize` has to be removed. Both methods are
only `no_state` when using the final heap which has a soundness
problem with constructors. There is currently no nicer way to do
this in KeY automatically. The Makefile takes care of this
adaptation.

* The methods `Tree::classify`, `Tree::classify_all` as well as `Tree::build` were left out as future work.

* To run the code use the `bench` branch which has the proper fallback sorting algorithm not commented out.

* The sampling function `Functions::select_n` is left empty and should probably be implemented.

## Publications

1. Axtmann, M., Ferizovic, D., Sanders, P., Witt, S.: [*Engineering
in-place (shared- memory) sorting
algorithms*](https://dl.acm.org/doi/full/10.1145/3505286). ACM
Transaction on Parallel Computing 9(1), 2:1– 2:62 (2022), see also
[github.com/ips4o](https://github.com/ips4o). Conference version in
ESA 2017

2. B. Beckert, P. Sanders, M. Ulbrich, J. Wiesler, and S. Witt:
*Formally Verifying an Efficient Sorter*. arxiv
Loading

0 comments on commit 4e58ad5

Please sign in to comment.