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
int32/avx2 version 20180729
takes about 143 seconds
on one core of
a 1.7GHz Intel Xeon E5-2609 v4 (Broadwell).
About 76% of this time is for
minmax, and 6% for
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
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
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
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
vpunpckinstructions. Otherwise angr will crash on djbsort.
angrpatch2.txt: Superseded by
angrpatch3.txt: Various peephole optimizations. Specifically: C idiom for signedmin; C idiom for signedmax;
concat(y,x)if lengths are multiples of 8;
concat(0,x)if lengths are multiples of 8; same for any combinations of reversals and zeros;
loware 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;
angrpatch4.txt: Portion of
angrpatch3.txtbeyond claripy commit
Version: This is version 2019.05.16 of the "Verification" web page.