Porting LARA
We need to port LARA from iGPS to GPFSL. The following files are to be ported:
- /logically_atomic.v → /logic/logically_atomic.v
- /invariants.v → /logic/obj_invariants.v
- /examples/snapshot.v → /examples/frac_auth.v and snapshot.v
-
/examples/hist_protocol.v? - /examples/list_lemmas.v → /base_logic/list_lemmas.v
- /examples/abs_hashtable.v → /examples/abs_hashtable.v
- /examples/hashtable.v
- /examples/for_loop.v → /logic/for_loop.v
- /examples/repeat.v → /logic/repeat.v
- /examples/kvnode.v → /examples/kvnode.v
- /examples/kvnode2.v
- /gps/shared2.v
-
recursive protocol?
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information