Commit 0a4a0da7 authored by Zhen Zhang's avatar Zhen Zhang

Modify module

parent bf584746
...@@ -9,4 +9,4 @@ ...@@ -9,4 +9,4 @@
*~ *~
*.bak *.bak
.coq-native/ .coq-native/
Makefile.coq Makefile*
-Q . iris -Q . flatcomb
incr.v incr.v
sync.v sync.v
pair_cas.v pair_cas.v
...@@ -2,8 +2,9 @@ From iris.program_logic Require Export weakestpre. ...@@ -2,8 +2,9 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics. From iris.proofmode Require Import invariants tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.tests Require Import atomic sync. From iris.tests Require Import atomic.
From iris.heap_lang Require Import spin_lock. From iris.heap_lang Require Import spin_lock.
From flatcomb Require Import sync.
Section sync_incr. Section sync_incr.
Context `{!heapG Σ, !lockG Σ} (N : namespace). Context `{!heapG Σ, !lockG Σ} (N : namespace).
......
...@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang. ...@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import excl. From iris.algebra Require Import excl.
From iris.tests Require Import sync. From flatcomb Require Import sync.
Import uPred. Import uPred.
(* CAS, load and store to pair of locations *) (* CAS, load and store to pair of locations *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment