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:

• unroll: An unroller that, given the compiled djbsort library, produces a fully unrolled program for arrays of the specified size. This converter is a small Python script built on top of the angr symbolic-execution tool introduced in 2016 Shoshitaishvili–Wang–Salls–Stephens–Polino–Dutcher–Grosen–Feng–Hauser–Kruegel–Vigna. This tool, in turn, builds upon the VEX library inside Valgrind.

• minmax: A peephole optimizer that converts the fully unrolled program to a sequence of "min" and "max" operations. To simplify this optimizer, djbsort has contributed some optimization patches to angr.

• decompose: A verifier that proves that the min-max program is a sorting program.

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:

• Decompose the min-max program into presumed 2-way-merging programs. The tool does not require the merge to be a merge of inputs on the left with inputs on the right; it allows arbitrary interleaving of the two lists of inputs (and djbsort uses interleaving for vectorizability). However, the 2-way-merging structure is essential; more general sorting programs cannot be verified with the current tool. For example, verifying the communication-efficient Schnorr–Shamir mesh sorting algorithm would require extending the tool to recognize the structure of that algorithm.

• Verify each presumed 2-way-merging program, by testing the program on a linear-size list of inputs. For example, a min-max program correctly merges all sequences of 3 inputs with all sequences of 5 inputs if and only if it correctly merges 0 1 2 with 3 4 5 6 7; 0 1 7 with 2 3 4 5 6; 0 6 7 with 1 2 3 4 5; and 5 6 7 with 0 1 2 3 4.

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:

• angrpatch1.txt: Support the AVX2 vpunpck instructions. Otherwise angr will crash on djbsort.

• angrpatch2.txt: Superseded by angrpatch3.txt.

• angrpatch3.txt: Various peephole optimizations. Specifically: C idiom for signedmin; C idiom for signedmax; reverse(concat(reverse(x),reverse(y))) ⇒ concat(y,x) if lengths are multiples of 8; reverse(concat(reverse(x),0)) ⇒ concat(0,x) if lengths are multiples of 8; same for any combinations of reversals and zeros; reverse(extract(reverse(x),high,low)) ⇒ extract(x,xbits-1-low,xbits-1-high) if xbits and high+1 and low are multiples of 8; concat(a,b) ^ concat(c,d) ⇒ concat(a^c,b^d) if sizes match; concat(a,b) & concat(c,d) ⇒ concat(a&c,b&d) if sizes match; (SignExt(n,v)>>s)[vbits-1:0] ⇒ v>>(s[vbits-1:0]) if n+vbits<2**(vbits-1).

• angrpatch4.txt: Portion of angrpatch3.txt beyond claripy commit 7826167ecb4f965acb55f7b0d3a4677588242c28.

---

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