Skip to content
Snippets Groups Projects
Select Git revision
  • ci/janno/reduction_no_check
  • ci/places
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/lia-experiment
  • ci/ralf/old-timing-data
  • ci/ralf/sections
  • ci/robbert/faster_iDestruct2
  • ci/robbert/iprop_structures
  • ci/robbert/merge_sbi
  • ci/robbert/merge_sbi_new
  • ci/robbert/merge_sbi_new_weak
  • ci/robbert/merge_sbi_weak
  • ci/robbert/naive_solver
  • ci/weak_mem
  • contractiveness
  • coqbug/match
  • fast_string
  • ghostcell
  • gpirlea/pinning
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
23 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.016Aug108432131Jul19171611107643220Jun18May171615131294229Apr282726252422201918141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov292827262524232216151110987Get rid of lft_inv_alive_twice, which was completely artificial.Rearranging lifetime.v. Changing the proof of bor_unnest: we do not need atomic accessors here.Use notations.Spurious imports.These are spurious laters.These EqDecision instances are not needed.Cleaning up the lifetime logic.Put the internal namespace definitions of the lifetime logic in the model.Put the shift_loc notation in the right scope so that it is parsed/printed properly even when appearing in expressions.Notation for shift_loc (finally \!).Tactical support for null comparison.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqMake valid comparisons between pointers and 0.unfix a FIXMEadd a note about the arc protocol so that it does not get lostFix a FIXME.Fix lines lenght.fix a commentprove rayon::joinadd comment to spawn verificationadd a stub for rayon::joinrenameAdd .gitattribute to ignore some files during the export.Anonymize.better explanation what goes on in panic.vREADMESimplify the model of mutexes by removing the exclusive token.SimplificationsMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqDerive unnesting and reborrowing from a common principle.Bump Iris.Lifetime logic: rename shared borrows to atomic (persistent) borrowsMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqComment on function type.expand on a commentMake emp be defined as the empty sum. Make panic return the empty type.Do not allow na reads and CAS to race on the same location.strong_cas_failstrong_cas_failMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqAn example with non-lexical lifetimes.explain a weird design choice