Skip to content

[catalogue] Fix catalogue #1939

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
maranget wants to merge 5 commits into
base: master
Choose a base branch
from
Open

[catalogue] Fix catalogue #1939

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
344f6e4
[catalogue] Partly restore the "demo" book.
maranget Jul 30, 2026
7942e2b
[catalogue] Fix herding-cats/ppc book
maranget Jul 30, 2026
1ea239f
[catalogue] Fix one "tiger" fence test in the tutorial book.
maranget Jul 30, 2026
026f9eb
[catalogue] Upate the tutorial "panther.cat" model.
maranget Jul 30, 2026
b369920
[herd,cat] Interpret one event `e` as a singleton in `[e]`
maranget Jul 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions catalogue/c11popl15/c11.cat-template
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,17 +1,18 @@
"C11"
withsc
withinit

(* Translation of C11 memory model from "Common Compiler Optimisations are *)
(* Invalid in the C11 Memory Model and what we can do about it" (POPL '15) *)

include "library.cat"
include "c11_cos.cat"
include "withsc.cat"

(* Simple aliases *)
let sb = singlestep(po) (* except po is a total per-thread order *)
let mo = co
let C = rmw
let scTotal = S (* total order over all SC actions due to 'withsc' option *)
(* total order over all SC actions due to 'include "withsc.cat"' *)
let scTotal = S
let imm = singlestep

(* --------------------------------------------------------------------------*)
Expand Down
1 change: 1 addition & 0 deletions catalogue/c11popl15/c11_cos.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
../../herd/libdir/c11_cos.cat
4 changes: 4 additions & 0 deletions catalogue/c11popl15/withsc.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
"Generate sc total orders"

let scbase = po|mo|rf|fr
with S from generate_orders(IW|sc,scbase)
3 changes: 3 additions & 0 deletions catalogue/demo/bells/anarchy.bell
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1,4 @@
"I can't dance"

enum ftype = 'ww || 'rr
instructions F[ftype]
3 changes: 3 additions & 0 deletions catalogue/demo/cats/anarchy.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
"I can't dance"

include "tutorial.cat"
11 changes: 11 additions & 0 deletions catalogue/demo/cats/basic.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
"common"

include "cross.cat"
include "filters.cat"

with co from generate_cos(co0)
let coe = co & ext
let fr = rf^-1;co
let fre = fr & ext
show co
show fr
3 changes: 1 addition & 2 deletions catalogue/demo/cats/c11.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
(* (Naive, SCnew, RSorig, STorig) *)
(* Autogenerated! Do not modify. *)
"C11"
withinit

(* Translation of C11 memory model from "Common Compiler Optimisations are *)
(* Invalid in the C11 Memory Model and what we can do about it" (POPL '15) *)
Expand All @@ -14,7 +13,7 @@ let sb = singlestep(po) (* except po is a total per-thread order *)
let mo = co
let C = RMW
let imm = singlestep
let asw = I * (M \ I)
let asw = IW * (M \ IW)

(* --------------------------------------------------------------------------*)
(* Figure 2: Auxiliary definitions *)
Expand Down
24 changes: 0 additions & 24 deletions catalogue/demo/cats/ptx.cat
View file
Open in desktop

This file was deleted.

3 changes: 3 additions & 0 deletions catalogue/demo/cats/tutorial.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
"I can't dance"

include "cos.cat"
28 changes: 0 additions & 28 deletions catalogue/demo/cfgs/cpp11.cfg
View file
Open in desktop

This file was deleted.

1 change: 1 addition & 0 deletions catalogue/demo/cfgs/cpp11.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
../../../herd/libdir/cpp11.cfg
29 changes: 14 additions & 15 deletions catalogue/demo/cfgs/tutorial.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,15 +1,14 @@
graph columns
squished true
showevents memory
showinitwrites false
fontsize 8
scale 0.75
xscale 1.0
yscale 0.6667
arrowsize 0.5
showfr true
showpoloc false
showinitrf true
showfinalrf false
splines spline
pad 0.1
graph columns
squished true
showevents memory
showinitwrites false
fontsize 8
scale 0.75
xscale 1.0
yscale 0.6667
arrowsize 0.5
doshow fr
showinitrf true
showfinalrf false
splines spline
pad 0.1
9 changes: 0 additions & 9 deletions catalogue/demo/shelf.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@
cats = [
"cats/x86.cat",
"cats/arm.cat",
"cats/ptx.cat",
"cats/c11.cat",
]

Expand All @@ -27,9 +26,6 @@
arm_tests = \
glob.glob("tests/*-arm*.litmus")

ptx_tests = \
glob.glob("tests/*-ptx*.litmus")

c11_tests = \
glob.glob("tests/*-c11*.litmus")

Expand All @@ -49,11 +45,6 @@
"cats": ["cats/arm.cat"],
"litmuses": arm_tests,
},
{
"bells": ["bells/anarchy.bell"],
"cats": ["cats/ptx.cat"],
"litmuses": ptx_tests,
},
{
"bells": ["bells/anarchy.bell"],
"cats": ["cats/c11.cat"],
Expand Down
2 changes: 1 addition & 1 deletion catalogue/demo/tests/mp-arm+dsb+addr.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
ARM MP+dsb+addr
ARM MP-arm+dsb+addr
{
%x0=x; %y0=y;
%y1=y; %x1=x;
Expand Down
2 changes: 1 addition & 1 deletion catalogue/demo/tests/mp-arm.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
ARM MP
ARM MP-ARM
{
%x0=x; %y0=y;
%y1=y; %x1=x;
Expand Down
9 changes: 9 additions & 0 deletions catalogue/demo/tests/mp-bell.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Bell MP-Bell
{
x = 0;
y = 0;
}
P0 | P1 ;
w[] x 1 | r[] r1 y ;
w[] y 1 | r[] r2 x ;
exists (1:r1 = 1 /\ 1:r2 = 0)
2 changes: 1 addition & 1 deletion catalogue/demo/tests/mp-x86.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
X86 MP
X86 MP-X86
{ x=0; y=0; }
P0 | P1 ;
MOV [x],$1 | MOV EAX,[y] ;
Expand Down
2 changes: 1 addition & 1 deletion catalogue/herding-cats/ppc/cats/ppc.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ let detour = po-loc & (coe;rfe)

let ii0 = dp | rdw | rfi
let ic0 = 0
let ci0 = ctrlcfence(ISYNC) | detour
let ci0 = ctrlcfence(ctrl,ISYNC) | detour
let cc0 = dp | po-loc | ctrl | (addr;po)

let rec ii = ii0 | ci | (ic;ci) | (ii;ii)
Expand Down
2 changes: 1 addition & 1 deletion catalogue/tutorial/cats/panther.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ let at-least-one k = (k * _ | _ * k)
let conflict = at-least-one(W) & loc & ext
let race =
let r = conflict & ~(hb | hb^-1)
in r \ (id | (I * M) | (M * I) | (Special * Special))
in r \ (id | (IW * M) | (M * IW) | (Special * Special))
show race

procedure race-free() =
Expand Down
2 changes: 1 addition & 1 deletion catalogue/tutorial/tests/sb+fwr+fwr.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,6 @@ y = 0;
}
P0 | P1 ;
w[] x 1 | w[] y 1 ;
f[wr] | f[wr] ;
f[hw] | f[hw] ;
r[] r1 y | r[] r2 x ;
exists (0:r1 = 0 /\ 1:r2 = 0)
12 changes: 7 additions & 5 deletions lib/interpreter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1372,6 +1372,7 @@ module Make
begin match eval_ord env e with
| V.Empty -> V.Empty
| Unv -> Rel (Lazy.force env.EV.ks.id)
| Event e -> Rel (E.EventRel.singleton (e,e))

@fsestini fsestini Jul 31, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Out of curiosity, what problem is this line addressing? What is an example of a ToId operator with an Event operand?

@maranget maranget Jul 31, 2026 •
edited
Loading

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well I could have made a separate PR the code is let succs (e,r) = range ([e];r), where e is a single event. This code was working before,because the Cat interpreter was systematically using the same function (eval_events) when an event set is expected. The function eval_events performs the silent promotion of one event into a singleton set. Since for instance PR #1855, the evaluation of sets has become more complex and this case of [e] where e is an event had been overlooked.

| Set s -> Rel (E.EventRel.set_to_rln s)
| v -> error_events env.EV.silent (get_loc e) v
end
Expand Down Expand Up @@ -1796,7 +1797,7 @@ module Make
and seq_args env = function
| [] -> Runv
| e::es ->
match eval_rels env e with
match eval_seq_arg env e with
| Runv -> seq_args env es
| Rid s -> seq_args_id env s es
| Revent r -> seq_args_rel env r es
Expand All @@ -1806,7 +1807,7 @@ module Make
let r =
List.fold_left
(fun r e ->
match eval_rels env e with
match eval_seq_arg env e with
| Rclass c -> ClassRel.sequence r c
| _ ->
error env.EV.silent (get_loc e)
Expand All @@ -1819,7 +1820,7 @@ module Make
match es with
| [] -> Rid s
| e::es ->
match eval_rels env e with
match eval_seq_arg env e with
| Runv -> seq_args_id env s es
| Rid t ->
seq_args_id env
Expand All @@ -1844,7 +1845,7 @@ module Make
match es with
| [] -> Revent r
| e::es ->
match eval_rels env e with
match eval_seq_arg env e with
| Runv -> seq_args_rel env r es
| Rid s ->
begin
Expand Down Expand Up @@ -1937,12 +1938,13 @@ module Make
| Unv -> Lazy.force env.EV.ks.unv
| v -> error_rel env.EV.silent (get_loc e) v

and eval_rels env e =
and eval_seq_arg env e =
match e with
| Op1 (_,ToId,e) ->
begin
match eval_ord env e with
| Set es -> Rid es
| Event e -> Rid (E.EventSet.singleton e)
| V.Empty -> raise Exit
| Unv -> Runv
| v -> error_events env.EV.silent (get_loc e) v
Expand Down
Loading