• Robbert Krebbers's avatar
    Modify the Hoare judgment such that is also ensures thread safity. · 9fcbbccf
    Robbert Krebbers authored
    Before, it just ensured that whenever one can split up the memory
    into two parts before running the program, the framing part can
    be split off when the program is finished. Now it also ensure that
    it can be split off at any moment during the execution of the
    program.
    
    When we extend to non-deterministic expressions/sequence points we
    certainly need this for the Hoare judgment for expressions, as C
    allows evaluation of them to interleave. However, for consistency,
    and further extensions, it is nice to have this property for
    statements too.
    9fcbbccf
fin_maps.v 11.5 KB