File: concurrency_interface_v2.sail

package info (click to toggle)
sail-ocaml 0.19.1%2Bdfsg5-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 18,008 kB
  • sloc: ml: 75,941; ansic: 8,848; python: 1,342; exp: 560; sh: 474; makefile: 218; cpp: 36
file content (200 lines) | stat: -rw-r--r-- 5,522 bytes parent folder | download
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
default Order dec

$define CONCURRENCY_INTERFACE_V2

$include <prelude.sail>
$include <concurrency_interface.sail>
$include <concurrency_interface/exception.sail>

val id_bits64 : bits(64) -> bits(64)

function id_bits64 bv = bv

val unit_true : unit -> bool
function unit_true () = true

val unit_false : unit -> bool
function unit_false () = true

val unit_zero : unit -> int
function unit_zero () = 0

instantiation sail_mem_read with
  'addr_size = 64,
  'addr_space = unit,
  'mem_acc = unit,
  mem_acc_is_explicit = unit_true,
  mem_acc_is_ifetch = unit_false,
  mem_acc_is_ttw = unit_false,
  mem_acc_is_relaxed = unit_true,
  mem_acc_is_rel_acq_rcpc = unit_false,
  mem_acc_is_rel_acq_rcsc = unit_false,
  mem_acc_is_standalone = unit_true,
  mem_acc_is_exclusive = unit_false,
  mem_acc_is_atomic_rmw = unit_false,
  'abort = bits(8),
  'CHERI = true,
  'cap_size_log = 3



instantiation sail_mem_write with
  'addr_size = 64,
  'addr_space = unit,
  'mem_acc = unit,
  mem_acc_is_explicit = unit_true,
  mem_acc_is_ifetch = unit_false,
  mem_acc_is_ttw = unit_false,
  mem_acc_is_relaxed = unit_true,
  mem_acc_is_rel_acq_rcpc = unit_false,
  mem_acc_is_rel_acq_rcsc = unit_false,
  mem_acc_is_standalone = unit_true,
  mem_acc_is_exclusive = unit_false,
  mem_acc_is_atomic_rmw = unit_false,
  'abort = bits(8),
  'CHERI = true,
  'cap_size_log = 3

enum my_barrier = Barrier1 | Barrier2

instantiation sail_barrier with 'barrier = my_barrier

register R1 : bits(64)
register R2 : bits(64)

val main : unit -> unit

function main() = {
    let w_req : Mem_write_request(8, 1, 64, unit, unit) = struct {
        access_kind = (),
        address = 0x0000_0000_0060_0000,
        address_space = (),
        size = 8,
        num_tag = 1,
        value = [0xAB, 0xCD, 0x12, 0x34, 0xFF, 0xFF, 0x56, 0x78],
        tags = [true]
    };
    print_bits("least significant byte = ", w_req.value[0]);
    match sail_mem_write(w_req) {
        Ok(_) => (),
        Err(abort) => {
            print_bits("abort = ", abort)
        }
    };
    let r_req : Mem_read_request(8, 0, 64, unit, unit) = struct {
        access_kind = (),
        address = 0x0000_0000_0060_0000,
        address_space = (),
        size = 8,
        num_tag = 0
    };
    match sail_mem_read(r_req) {
        Ok((value, v)) => {
            print_bits("read memory (no tag read) = ", from_bytes_le(value))
        },
        _ => print_endline("invalid read"),
    };
    let r_req : Mem_read_request(4, 0, 64, unit, unit) = struct {
        access_kind = (),
        address = 0x0000_0000_0060_0000,
        address_space = (),
        size = 4,
        num_tag = 0
    };
    match sail_mem_read(r_req) {
        Ok((value, v)) => {
            print_bits("read memory 4 lower bytes (no tag read) = ", from_bytes_le(value))
        },
        _ => print_endline("invalid read"),
    };
    let r_req : Mem_read_request(4, 0, 64, unit, unit) = struct {
        access_kind = (),
        address = 0x0000_0000_0060_0004,
        address_space = (),
        size = 4,
        num_tag = 0
    };
    match sail_mem_read(r_req) {
        Ok((value, v)) => {
            print_bits("read memory 4 higher bytes (no tag read) = ", from_bytes_le(value))
        },
        _ => print_endline("invalid read"),
    };

    sail_barrier(Barrier1);
    let r_req : Mem_read_request(8, 1, 64, unit, unit) = struct {
        access_kind = (),
        address = 0x0000_0000_0060_0000,
        address_space = (),
        size = 8,
        num_tag = 1,
    };
    match sail_mem_read(r_req) {
        Ok((value, v)) if v[0] => {
            print_bits("read memory (true tag) = ", from_bytes_le(value))
        },
        _ => print_endline("invalid read"),
    };

    let w_req : Mem_write_request(2, 0, 64, unit, unit) = struct {
        access_kind = (),
        address = 0x0000_0000_0060_0002,
        address_space = (),
        size = 2,
        num_tag = 0,
        value = [0xDE, 0xAD],
        tags = []
    };
    match sail_mem_write(w_req) {
        Ok(_) => (),
        Err(abort) => {
            print_bits("abort = ", abort)
        }
    };
    let r_req : Mem_read_request(8, 1, 64, unit, unit) = struct {
        access_kind = (),
        address = 0x0000_0000_0060_0000,
        address_space = (),
        size = 8,
        num_tag = 1,
    };
    match sail_mem_read(r_req) {
        Ok((value, v)) if v[0] == false => {
            print_bits("read memory (false tag) = ", from_bytes_le(value))
        },
        _ => print_endline("invalid read"),
    };

    let r_req : Mem_read_request(2, 1, 64, unit, unit) = struct {
        access_kind = (),
        address = 0x0000_0000_0060_0002,
        address_space = (),
        size = 2,
        num_tag = 1,
    };
    match sail_mem_read(r_req) {
        Ok((value, v)) if not_bool(v[0]) => {
            print_bits("read memory 2 bytes (false tag) = ", from_bytes_le(value))
        },
        _ => print_endline("invalid read"),
    };

    /* Cycle count primitives */
    sail_end_cycle();
    let c = sail_get_cycle_count();
    print_int("c = ", c);

    /* Instruction and branch announce events */
    sail_instr_announce(0xABCD_1234);
    sail_branch_announce(64, 0x0000_0000_0000_4000);

    /* Isla relaxed register support */
    sail_reset_registers();
    sail_synchronize_registers();

    /* Isla mark register builtins */
    sail_mark_register(ref R1, "MARK");
    sail_mark_register_pair(ref R1, ref R2, "MARK2");

    print_bits("", __monomorphize(0xFFFF));
}