Challenge 7: make panicking part optional; remove mention of verifying intrinsics

[carolynzech]

Update the atomic intrinsics challenge to make verifying the intrinsics out of scope, since that would require verifying compiler implementations that are out of scope for this effort. Also make the part about verifying the absence of panics optional to restrict the requirements to safety only.

I also added a mdbook-linkcheck dependency because I discovered I needed that to build the book locally.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[carolynzech]

Two things that @remi-delmas-3000 and I discussed offline:

1. Rather than asking to "verify" the intrinsics, we can add a stretch goal to add specifications for the intrinsics' behavior. The idea is that each verification tool is going to have its own model of how the intrinsics behave, so it'd be nice to have sort of baseline spec that tool authors could reference.
2. The challenge has "data races" as one of the undefined behaviors to prevent. What precisely does this mean?
   The atomics documentation says:

A data race is defined as conflicting non-synchronized accesses where at least one of the accesses is non-atomic. Here, accesses are conflicting if they affect overlapping regions of memory and at least one of them is a write. They are non-synchronized if neither of them happens-before the other, according to the happens-before order of the memory model.
The other possible cause of undefined behavior in the memory model are mixed-size accesses: Rust inherits the C++ limitation that non-synchronized conflicting atomic accesses may not partially overlap. In other words, every pair of non-synchronized atomic accesses must be either disjoint, access the exact same memory (including using the same access size), or both be reads.

From @remi-delmas-3000:

1. Should the contract for each atomic method talk about all the things another thread is allowed to do while this method executes in one thread?
2. Should these be global properties that the verifiers must instantiate automatically?
3. What would a proof of absence of UB in a single method look like, if any other thread can cause UB by accessing the atomic behind our back?

We don't necessarily need to resolve these issues in this pull request, but it'd be good to get the discussion going.

[btj]

Re data races: this is fairly easy to enforce using separation logic, as I'm doing in my WIP solution to this challenge.