projects / userspace-rcu.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9d95031) | patch
Add ooomem and urcu checks
authorMathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Mon, 23 Feb 2009 05:53:37 +0000 (00:53 -0500)
committerMathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Mon, 23 Feb 2009 05:53:37 +0000 (00:53 -0500)
commit60a1db9d10aaca98e79a5126f168a37d00151845
tree90def38e89f3e3c887122f61e59b519cc420fd65tree | snapshot
parent9d95031158c22e376007c862e52652d267414e5ecommit | diff
Add ooomem and urcu checks

Create a more simple model for ooo memory accesses and basic urcu checks.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
17 files changed:
formal-model/ooomem/DEFINES [new file with mode: 0644] blob
formal-model/ooomem/Makefile [new file with mode: 0644] blob
formal-model/ooomem/mem.sh [new file with mode: 0644] blob
formal-model/ooomem/mem.spin [new file with mode: 0644] blob
formal-model/ooomem/read_order.ltl [new file with mode: 0644] blob
formal-model/ooomem/read_order_no_rmb.define [new file with mode: 0644] blob
formal-model/ooomem/read_order_no_wmb.define [new file with mode: 0644] blob
formal-model/ooomem/references.txt [new file with mode: 0644] blob
formal-model/urcu/DEFINES [new file with mode: 0644] blob
formal-model/urcu/Makefile [new file with mode: 0644] blob
formal-model/urcu/references.txt [new file with mode: 0644] blob
formal-model/urcu/urcu.sh [new file with mode: 0644] blob
formal-model/urcu/urcu.spin [new file with mode: 0644] blob
formal-model/urcu/urcu_free.ltl [new file with mode: 0644] blob
formal-model/urcu/urcu_free_no_mb.define [new file with mode: 0644] blob
formal-model/urcu/urcu_free_no_rmb.define [new file with mode: 0644] blob
formal-model/urcu/urcu_free_no_wmb.define [new file with mode: 0644] blob
Userspace RCU (urcu) for Linux
This page took 0.025152 seconds and 4 git commands to generate.