Missing support for negated sets and Aborted execution

[hernanponcedeleon]

The following cat file

let ext = ext & ((~IW) * M)
let int = int | (IW * M)
let rfe = rf & ext
let coe = co & ext
let fre = fr & ext
let rfi = rf & int
let coi = co & int
let fri = fr & int

(** Atomicity **)
assume rmw & (fre;coe) <= 0

(** SC per location **)
let uniproc = (co | rf | fr | po-loc)^+ & id
assume uniproc <= 0

let Marked = RLX | ACQ | REL | SC
let Plain = ~Marked
let Acq = ACQ | (SC & R)
let Rel = REL | (SC & W)

let carry-dep = data;rfi | addr | ctrl
let ctrl = carry-dep* ; ctrl
let addr = carry-dep* ; addr
let data = carry-dep* ; data
let dep = ctrl | addr | data

let bob = [Acq];po | po;[Rel] | [SC];po;[SC] | po;[SC & F];po | [R];po;[Acq & F];po | po;[Rel & F];po;[W & Marked]
let ppo = bob | [Marked];(dep | coi | fri);[W & Marked]

let WRF-ppo = po;[Rel & F];po;[W & Plain] | [Marked];(ctrl | addr);[W & Plain]

let hb = (ppo | WRF-ppo | rfe | fre | coe)^+ & id
assume hb <= 0

shows two problems

• There is lack of support for negated sets (or are you using a symbol different than cat)
• Even if I removed the negations, rat returns

  terminate called after throwing an instance of 'std::bad_variant_access'
  what():  std::get: wrong index for variant
  Aborted (core dumped)

[ThomasHaas]

Negated sets are not supported. I'm not sure if it is even possible (negated relations surely are not supported). You have to approximate negations like this:

let Marked = ...
assume Plain & Marked <= 0 // Plain and Marked are mutually exclusive

While this will guarantee disjoint Plain/Marked sets, it allows for events that are neither Plain nor Marked.

[ThomasHaas]

The second is probably due to let WRF-ppo = po;[Rel & F];po;[W & Plain] | [Marked];(ctrl | addr);[W & Plain]. Currently, the tool assumes all relations starting with a capital letter are unary and otherwise binary. Can you try renaming the relation to wrf-ppo?

[hernanponcedeleon]

Can you try renaming the relation to wrf-ppo?

This worked

[hernanponcedeleon]

Negated sets are not supported. I'm not sure if it is even possible (negated relations surely are not supported).

Assuming sets are static, this should not be an issue right? Once could statically rewrite the nagation

[ThomasHaas]

There is no notion of "static" in this tool. How would you rewrite the negation? I can only think of a rather complex way to do rewriting, where you introduce a "universe" set like this:

let U = Marked | Plain
assume Marked & Plain <= 0

And restrict every base relation to be in the universe:

let rf = [U];rf;[U]
let co = [U];co;[U]
...

If you want to split the universe by even more criteria (e.g. into R/W/F), it gets really ugly. EDIT: It's not so ugly, see below.

[ThomasHaas]

@jangreen Isn't the above a complete technique to handle arbitrary coverings of the universe? More precisely, suppose you want to cover (not necessarily disjointly) the universe U in various ways e.g., U = R | W | F and U = Marked | Plain then you can do the following rewriting

let U1 = R | W | F
let U2 = Marked | Plain

// For all base relations b
let b = [U2];[U1];b;[U1];[U2]  // or equivalently [U1 & U2];b;[U1 & U2]

If desired, you can make the coverings disjoint using assumptions:

// U1
assume R & (W | F) <= 0
assume W & F <= 0
// U2
assume Marked & Plain <= 0

In particular, this allows you to define negations of arbitrary sets. IIRC, emptiness assumptions are complete, so this would even give you complete handling of set negations, no? I find this quite surprising (if it is true) because it would imply that either negations of domain/range-projections of binary relations can also be handled completely or that such projections are not complete to begin with (even without negation).

[jangreen]

I think it is correct that you can express negations in terms of a universe U, as you have done. However, it is not possible to express assumptions like Top = R | W | F, because that would require that derived relations can occur on the rhs of assumptions.

[ThomasHaas]

Would you ever need TOP if you relativize everything to a universe though?