libs: Simplify implementations of thread parking and guard::enable

[RyanGlScott]

Fixes #226.

[spernsteiner]

IIRC crux-mir has some limited support for verifying multithreaded programs. Is that now going to silently misbehave on programs that call park()?

[RyanGlScott]

Truth be told, I don't have a whole lot of insight into the concurrency-related parts of crux-mir. (As I understand it, they consist of a handful of concurrency-related primitives, for which crux-mir provides overrides for here.)

FWIW, none of the test cases under crux-mir/test/concurrency, so I'm not even clear if park() is intended to be under the scope of crux-mir's concurrency support.

[spernsteiner]

My worry is that where previously it would crash in an obvious way if your program calls park(), now it may silently produce unsound results. For example, if the concurrency support is meant to explore all possible interleavings, it will miss some interleavings because the unsupported version of park() doesn't include any operations that could trigger a context switch.

[RyanGlScott]

Fair enough. How should we proceed, then? Should we try implementing our own configuration of thread parking in terms of the concurrency-related primitives? If so, I'll likely need some guidance here, as I'm not at all familiar with this part of the code.

[spernsteiner]

Hmm, I was going to suggest implementing parking in terms of Mutex and Condvar, on the assumption that those are already calling the necessary Crucible concurrency hooks, but it turns out Condvar is also implemented as a bunch of no-ops. So probably the best path forward here is to stick with the no-op parker, and maybe document that the crux-mir concurrency support is currently broken/bitrotted. (Aside from Condvar, it looks like the various atomic types are also missing calls to concurrency hooks—see GaloisInc/crucible@b38fdfb.)

[RyanGlScott]

Ah, right. I opened #238 a while back about this, so it would be good to cite that issue here.

[RyanGlScott]

I've done this in d2a690b.