djbsort

djbsort includes tools that, given an array size, automatically verify correctness of djbsort's output for all possible input arrays of that size. These tools have three parts:

The time to run the whole sequence of tools gradually increases with the array size. For array size 1024, running the whole sequence of tools to verify int32/avx2 version 20180729 takes about 143 seconds on one core of bolero, a 1.7GHz Intel Xeon E5-2609 v4 (Broadwell). About 76% of this time is for unroll, 14% for minmax, and 6% for decompose. The remaining time is spent simulating the intermediate programs to double-check that they sort a pseudorandom input.

Internally, the verifier has two components:

The fact that a quadratic-size list of test bits is enough for a merging network (whereas the best known methods to test a general sorting network are much slower) is noted in Knuth's Art of Computer Programming. The fact that larger test inputs allow a linear-size list (analogously to an older speedup by Yao for general sorting networks) was pointed out in 1987 Chung–Ravikumar. However, the test set stated in that paper is too small (off by one). A correct test set appears in 2007 Even–Levi–Litman. Both of these papers consider only the balanced case, merging n/2 inputs with n/2 inputs, but the idea generalizes immediately to other cases.

How to install angr and verify djbsort

These instructions were tested on a virtual machine (created with xen-create-image) running the latest release ("unstable") of Debian.

As root, install various libraries and development packages:

    dpkg --add-architecture i386
    apt update
    apt dist-upgrade -y
    apt install \
      man wget strace psmisc screen vim time git tig \
      build-essential clang gdb valgrind nasm cmake \
      libffi-dev libssl-dev libxml2-dev libxslt1-dev \
      libreadline-dev libpixman-1-dev libqt4-dev \
      libglib2.0-dev python-dev python2.7-dev pypy \
      python3 python-pip virtualenvwrapper pypy-dev \
      python-pyparsing python3-pyparsing \
      python3-pip \
      libtool debootstrap debian-archive-keyring \
      binutils-multiarch libc6:i386 libgcc1:i386 \
      libstdc++6:i386 libtinfo5:i386 zlib1g:i386 \
      multiarch-support gcc-multilib \
      -y

Now start a new shell as the user that compiled djbsort. Install angr in a Python 3 virtual environment:

    cd
    mkvirtualenv -p /usr/bin/python3 angr
    pip install angr

Run the verifymany script to verify sorting for all small sizes:

    workon angr
    pip install pyparsing
    cd
    version=$(cat sorting.cr.yp.to/djbsort-latest-version.txt)
    cd djbsort-$version/verif
    ./verifymany

The verifymany script stops with an error message if it encounters any failures.

The angr patches

In case the history is of interest, description of the patches contributed by djbsort to angr:


Version: This is version 2019.08.31 of the "Verification" web page.