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

type instruction =
  | Store of int * int64 | Load of int * int | Fence
  | Move of int * int64 | Branch of int * int64 * int
  | Enter | Leave | Exchange of int * int * int64

type goal = Overlap | Outcome of {
  registers : (int * int * int64) list;
  memory : (int * int64) list;
  drained : bool;
}

type model = Sc | Tso
type location = int * int
type t = {
  name : string;
  names : string array;
  bound : int;
  threads : instruction array array;
  candidates : location list;
  goal : goal;
}

let model = function "sc" -> Sc | "tso" -> Tso | _ -> invalid_arg "unknown memory model"
let model_name = function Sc -> "sc" | Tso -> "tso"
let location value = match Sexp.list value with
  | [t; pc] -> Sexp.integer t, Sexp.integer pc
  | _ -> invalid_arg "invalid fence location"

let instruction value =
  let open Sexp in
  match value with
  | Store (a, v) -> List [Atom "store"; i a; w v]
  | Load (a, r) -> List [Atom "load"; i a; i r]
  | Fence -> List [Atom "fence"]
  | Move (r, v) -> List [Atom "move"; i r; w v]
  | Branch (r, v, target) -> List [Atom "branch"; i r; w v; i target]
  | Enter -> List [Atom "enter"]
  | Leave -> List [Atom "leave"]
  | Exchange (a, r, v) -> List [Atom "exchange"; i a; i r; w v]

let decode_instruction value =
  let open Sexp in
  match list value with
  | [Atom "store"; a; v] -> Store (integer a, word v)
  | [Atom "load"; a; r] -> Load (integer a, integer r)
  | [Atom "fence"] -> Fence
  | [Atom "move"; r; v] -> Move (integer r, word v)
  | [Atom "branch"; r; v; target] -> Branch (integer r, word v, integer target)
  | [Atom "enter"] -> Enter
  | [Atom "leave"] -> Leave
  | [Atom "exchange"; a; r; v] -> Exchange (integer a, integer r, word v)
  | _ -> invalid_arg "invalid instruction"

let validate case =
  let check condition message = if not condition then invalid_arg message in
  check (Array.length case.threads = 2) "exactly two threads required";
  check (Array.length case.names > 0 && Array.length case.names <= 16) "address count outside 1..16";
  check (case.bound > 0 && case.bound <= 64) "step bound outside 1..64";
  let address a = check (a >= 0 && a < Array.length case.names) "address outside model" in
  let register r = check (r >= 0 && r < 4) "register outside model" in
  Array.iter (fun program ->
    check (Array.length program > 0 && Array.length program <= 64) "thread length outside 1..64";
    Array.iter (function
      | Store (a, _) -> address a
      | Load (a, r) | Exchange (a, r, _) -> address a; register r
      | Move (r, _) -> register r
      | Branch (r, _, target) -> register r;
          check (target >= 0 && target <= Array.length program) "branch target outside thread"
      | Fence | Enter | Leave -> ()) program) case.threads;
  let thread t = check (t >= 0 && t < 2) "thread outside model" in
  List.iter (fun (t, pc) -> thread t;
    check (pc >= 0 && pc < Array.length case.threads.(t)) "fence outside thread") case.candidates;
  check (List.length case.candidates = List.length (List.sort_uniq compare case.candidates)) "duplicate fence";
  match case.goal with
  | Overlap -> ()
  | Outcome goal ->
      List.iter (fun (t, r, _) -> thread t; register r) goal.registers;
      List.iter (fun (a, _) -> address a) goal.memory

let singleton = function [value] -> value | _ -> invalid_arg "expected one field value"

let decode value =
  let open Sexp in
  let fields = match value with
    | List (Atom "case" :: fields) -> fields
    | _ -> invalid_arg "expected case"
  in
  let get key = singleton (field key fields) in
  let goal = match field "goal" fields with
    | [Atom "overlap"] -> Overlap
    | [List (Atom "outcome" :: fields)] ->
        let registers = List.map (fun value -> match list value with
          | [t; r; v] -> integer t, integer r, word v
          | _ -> invalid_arg "invalid register goal") (field "registers" fields) in
        let memory = List.map (fun value -> match list value with
          | [a; v] -> integer a, word v
          | _ -> invalid_arg "invalid memory goal") (field "memory" fields) in
        let drained = match field "drained" fields with
          | [Atom "true"] -> true | [Atom "false"] -> false
          | _ -> invalid_arg "invalid drain flag" in
        Outcome {registers; memory; drained}
    | _ -> invalid_arg "invalid goal"
  in
  let case = {
    name = atom (get "name");
    names = Array.of_list (List.map atom (field "names" fields));
    bound = integer (get "bound");
    threads = Array.of_list (List.map (fun thread ->
      Array.of_list (List.map decode_instruction (list thread))) (field "threads" fields));
    candidates = List.map location (field "candidates" fields);
    goal;
  } in
  validate case;
  case

let encode case =
  let open Sexp in
  let goal = match case.goal with
    | Overlap -> Atom "overlap"
    | Outcome goal -> List [Atom "outcome";
        List (Atom "registers" :: List.map (fun (t, r, v) -> List [i t; i r; w v]) goal.registers);
        List (Atom "memory" :: List.map (fun (a, v) -> List [i a; w v]) goal.memory);
        List [Atom "drained"; Atom (string_of_bool goal.drained)]] in
  List [Atom "case"; List [Atom "name"; Atom case.name];
    List (Atom "names" :: Array.to_list (Array.map a case.names));
    List [Atom "bound"; i case.bound];
    List (Atom "threads" :: Array.to_list (Array.map (fun thread ->
      List (Array.to_list (Array.map instruction thread))) case.threads));
    List (Atom "candidates" :: List.map (fun (t, pc) -> List [i t; i pc]) case.candidates);
    List [Atom "goal"; goal]]

let load path = decode (Sexp.one (Store.read path))