• Dan Frumin's avatar
    Simplify the Treiber stack refinement · bf38948f
    Dan Frumin authored
    The simplification is acheieved by removing the stackUR workaround.
    That RA was used to enusure that the nodes that were parts of the
    stack do not change themselves -- this is crucial for the safety of
    pop and iter operations.
    
    Now this is achieved by using duplicable propositions (∃ q, n ↦ᵢ{q} v)
    to ensure that the node are still alive/not freed.
    bf38948f
Name
Last commit
Last update
ci @ 9028d6c1 Loading commit data...
docs Loading commit data...
theories Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.gitmodules Loading commit data...
Makefile Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
awk.Makefile Loading commit data...
comments.org Loading commit data...
opam Loading commit data...