Github: related to #47 "properties, covers, etc"

The broader plan here is to do the final liveness check in parallel, rather than
single-threaded as originally planned. This should speed it up, but it also
means we need some rendezvous logic in exit_with() rather than simply ending.

Github: related to #47 "properties, covers, etc"

This is currently unused, but we now have a second, independent rendezvous point
available. The long term idea here is to have all threads rendezvous in
exit_with() using this second point, *after* opting out of the first rendezvous
point. After they've synchronised using this, they can go on in a next phase to
complete liveness checks. This ensures no threads overlap exploration and
liveness checking which avoids some messy scenarios. E.g. one thread wanting to
expand and migrate the seen set while another is probing its liveness. The delay
at the second rendezvous point should be acceptable because all threads should
be noticing someone has flipped the done flag and proceeding to a timely exit
anyway.

Github: related to #47 "properties, covers, etc"

Github: related to #47 "properties, covers, etc"

Github: related to #47 "properties, covers, etc"

Github: related to #47 "properties, covers, etc"

This is still not complete because we need to do a final pass through the
liveness check at the end and also signal errors if we fail the check.

Github: related to #47 "properties, covers, etc"

Github: related to #47 "properties, covers, etc"

Github: related to #47 "properties, covers, etc"

Github: related to #47 "properties, covers, etc"

These don't yet go on to generate any code, but the eventual plan is to check
these in the verifier.

Github: related #47 "properties, covers, etc"

We simply enable all the latest POSIX extensions at time of writing.

We never alter the signal mask, so it's an unnecessary overhead to save and
restore it when using a jmp_buf. This should speed up the verifier when using
assumptions and/or reporting multiple errors. This only occurred to me when
reading Dmitry Vyukov's blog, 1024 Cores.

Github: related to #50 "sandbox checker"

Github: related to #50 "sandbox checker"

By reducing this function to only read the ptr member of the struct, we can
avoid more expensive operations on some platforms. E.g. on x86-64, this lets us
drop a CMPXCHG16B followed by some juggling, for a regular 64-bit MOV.

Github: related to #104 "remove set_expand_lock?"

When the verifier is single threaded, there's no need to use a mutex or snoop
what other threads are doing. This allows us to optimise single threaded
checking slightly.

Github: related to #104 "remove set_expand_lock?"

As described in the comment, this is an optimisation for multithreaded
execution.

Github: closes #104 "remove set_expand_lock?"

This will be required for upcoming changes that allow reads to race with this
operation.

Github: related to #104 "remove set_expand_lock?"

OK, let's unpack that cryptic headline a little... When the seen set exceeds a
certain capacity, it gets expanded. The new set is allocated by one thread and
then all threads participate in the migration of the contents of the old set to
the new one. To arbitrate which thread is operating on any particular chunk of
the old set they use a shared counter, next_migration.

Prior to this commit, the counter was reset immediately preceding a migration.
Following this commit, we do the reset at the other end, after a migration. It
should be clear that the reset has to happen some time (so the counter starts at
zero the next time the set needs to be expanded) but it is valid to do it at
either end. The motivation for moving it to the end, is that we can do it in a
single-threaded context. This is during what I've referred to above as the
"rendezvous interstice." All threads arrive at the post-migration rendezvous
point and block on a condition variable. The last thread to arrive is designated
the "leader" and allowed a window of single-threaded execution before unblocking
all the "followers." By putting the reset in this window, we guarantee it gets
done in a way that (a) will not affect any ongoing migrations and (b) will be
observable by all other threads at the start of the next migration.

"But why did it need to move?" I hear you ask. It was already in a location that
was a single-threaded context enforced by the set expansion mutex. Well, we are
about to introduce an optimisation based on double-checked locking that allows
threads to observe a set expansion has already started without acquiring the set
expansion mutex. That is, they will be able to enter set_migrate having never
acquired the set expansion mutex. This means, if the counter reset was left
where it was, they could start migration work before the counter had been reset.
This could be resolved by moving the counter reset ahead of the write to
next_global_seen (what the DCLP check looks at) and adding some memory barriers
but it's simpler to just move the reset out of this path to a safer location
altogether.

Github: related to #104 "remove set_expand_lock?"

This avoids an unnecessary increment, then decrement of the pointer we're just
trying to read.

Github: related to #104 "remove set_expand_lock?"

This will allow us to avoid the awkward get+put we do to read the pointer's
value in set_expand.

Github: related to #104 "remove set_expand_lock?"

Some compilers do not treat typeof as a synonym and only recognise their own
built-in, __typeof__ or __typeof. This was not picked up before because it seems
we are not testing on any non-x86-64 platforms. It would be nice to address this
but I don't currently have any other platforms available.

Travis CI's environment is flaky enough that steps that retrieve things from the
network like this one often fail. To try to avoid the spurious failures and need
to manually restart we wrap it in Travis' retry script.

These are not defined in the version of Flex that ships with NetBSD 8.0, so just
expand them.

Some more paranoid toolchains (e.g. OpenBSD 6.4's default) warn about the use of
sprintf as an insecure function. Our usage is pretty contained, but we rephrase
this to keep such compilers happy.

Some platforms (e.g. FreeBSD) report this instead of x86_64. With this, Rumur
now supports FreeBSD.

This is probably as far back as we'll go with GCC compatibility, but it's
helpful to support 4.7 because this is installed in a number of base Linux
distros.

GCC 4.7 does not support these.

Github: related to #44 "drop width member of handle"

We effectively canonicalise handles by ensuring the base always points at the
first byte we would read and the offset is then only the bit offset within this
byte. The purpose of this is to eventually allow reducing the offset member to 3
bits.

Github: related to #44 "drop width member of handle"

This should have no effect on functionality, but just more closely uses the
state_handle abstraction to support upcoming changes.

Github: related to #44 "drop width member of handle"

This turned out to be surprisingly easy to address as the name in a quantifier
is merely a string member, and not an ExprID as I had thought.

Github: closes #103 "AST dump: quantified expressions don't output name"

An attempt to avoid the 50 minute timeout Travis places on tasks.

Github: closes #116 "work around Travis timeouts"

Github: related to #116 "work around Travis timeouts"