isla-axiomatic 0.2.0

Isla is a symbolic execution engine for Sail instruction set architecture specifications. This crate implements utilities for handling axiomatic memory models.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62

(declare-fun co (Event Event) Bool)

; co is irreflexive
(assert (forall ((ev Event))
  (not (co ev ev))))

; co is transitive
(assert (forall ((ev1 Event) (ev2 Event) (ev3 Event))
  (=>
    (and (co ev1 ev2) (co ev2 ev3))
    (co ev1 ev3))))

; Two distinct writes to the same location are co-related
(assert (forall ((ev1 Event) (ev2 Event))
  (=>
    (and (not (= ev1 ev2))
         (W ev1)
         (W ev2)
         (loc ev1 ev2))
    (or (co ev1 ev2) (co ev2 ev1)))))

; All writes are coherence order after the initial write
(assert (forall ((ev Event))
  (=> (W ev) (co IW ev))))

; All co-ordered writes must be to the same location if not the initial write
(assert (forall ((ev1 Event) (ev2 Event))
  (=> (and (not (= ev1 IW)) (co ev1 ev2)) (loc ev1 ev2))))

; co is total
(assert (forall ((ev1 Event) (ev2 Event))
  (=>
    (and (not (= ev1 ev2))
         (exists ((ev3 Event))
           (and (co ev1 ev3)
                (co ev2 ev3))))
    (or (co ev1 ev2) (co ev2 ev1)))))

; All co-ordered events are writes
(assert (forall ((ev1 Event) (ev2 Event))
  (=>
    (co ev1 ev2)
    (and (or (= ev1 IW) (W ev1)) (W ev2)))))

(declare-fun rf (Event Event) Bool)

; A read can only read from a single event
(assert (forall ((ev1 Event) (ev2 Event) (ev3 Event))
  (=> (and (rf ev1 ev2) (rf ev3 ev2))
      (= ev1 ev3))))

; Reads are paired with writes
(assert (forall ((ev1 Event) (ev2 Event))
  (=> (rf ev1 ev2)
      (or (and (W ev1) (loc ev1 ev2) (rw-pair ev1 ev2))
          (and (= ev1 IW) (r-initial ev2))))))

; All reads read from somewhere
(assert (forall ((ev1 Event))
  (=>
    (R ev1)
    (exists ((ev2 Event)) (rf ev2 ev1)))))