lukeg101

@INPROCEEDINGS{10444836,
  author={Geeson, Luke and Smith, Lee},
  booktitle={2024 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)}, 
  title={Compiler Testing with Relaxed Memory Models}, 
  year={2024},
  volume={},
  number={},
  pages={334-348},
  keywords={Concurrent computing;Industries;Codes;Computer bugs;Memory architecture;Programming;Testing;D.1.3 Concurrent Programming;B.1.2.b Formal models;B.1.4.b Languages and compilers;D.2.5.r Testing tools},
  doi={10.1109/CGO57630.2024.10444836}}

lukeg101

@misc{
  geeson2024fowm,
  title = {Weak Memory Demands Model-based Compiler Testing}, 
  author = {Luke Geeson},
  month = "January",
  year = {2024},
  eprint = {2401.09474},
  archivePrefix = {arXiv},
  primaryClass = {cs.PL},
  series = {The Future of Weak Memory Workshop (FOWM'24)},

lukeg101

AArch64 LB+CAS

{
0:X0=x; 0:X3=y;
1:X0=y; 1:X3=x;
}
 P0                 | P1          ;
label: LDXR W1,[X0] | LDR W1,[X0] ;
 STXR W4, W1, [X0]  | NOP ;
 CBNZ W4, label     | NOP;

lukeg101

{ [P0_r0]=0;[P1_r0]=0;[x]=0;[y]=0;
  uint64_t %P0_P0_r0=P0_r0;uint64_t %P0_x=x;uint64_t %P0_y=y;
  uint64_t %P1_P1_r0=P1_r0;uint64_t %P1_x=x;uint64_t %P1_y=y }

  P0                    |  P1                    ;
   MOV W10,#1           |   MOV W10,#1           ;
   LDR W8,[X%P0_x]      |   LDR W8,[X%P1_y]      ;
   CBZ W8, label1       |   CBZ W8, label2       ;
label1:                 | label2:                ;
   STR W10,[X%P0_y]     |   STR W10,[X%P1_x]     ;

lukeg101

{ [P0_r0]=0;[P1_r0]=0;[x]=0;[y]=0;
  uint64_t %P0_P0_r0=P0_r0;uint64_t %P0_x=x;uint64_t %P0_y=y;
  uint64_t %P1_P1_r0=P1_r0;uint64_t %P1_x=x;uint64_t %P1_y=y }

  P0                    |  P1                    ;
   MOV W10,#1           |   MOV W10,#1           ;
   LDR W8,[X%P0_x]      |   LDR W8,[X%P1_y]      ;
   STR W10,[X%P0_y]     |   STR W10,[X%P1_x]     ;
   STR W8,[X%P0_P0_r0]  |   STR W8,[X%P1_P1_r0]  ;

lukeg101

{ *x = 0, *y = 0 } // fixed initial state, shared memory x and y

// Concurrent Program with threads P0 and P1
P0 (atomic_int* y,atomic_int* x) {
  int r0 = atomic_load_explicit(x,memory_order_relaxed);
  atomic_store_explicit(y,1,memory_order_relaxed);
}

P1 (atomic_int* y,atomic_int* x) {
  int r0 = atomic_load_explicit(y,memory_order_relaxed);

lukeg101

from enum import Enum
import math
import random

# Tokens on the board are either Noughts, Crosses, or Empty
class Token(Enum):
    Nought = 'O'
    Cross  = 'X'
    Empty  = ' '

lukeg101

module Parser where

import Omega
import Control.Applicative (Applicative(..))
import Control.Monad       (liftM, ap, guard)
import Data.Char

{-
Implementation based on ideas in Monadic Parser Combinators paper
http://www.cs.nott.ac.uk/~pszgmh/monparsing.pdf

lukeg101

data Label = R | B
    deriving Show
data RBTree a = L | I a Label (RBTree a) (RBTree a)
    deriving Show

memberRBTree :: (Ord a) => a -> RBTree a -> Bool
memberRBTree a L = False
memberRBTree a (I x _ l r)
    | a == x = True
    | a <  x = memberRBTree a l

lukeg101

module BinomialTree where

data BinTree a = B Int a [BinTree a]
    deriving Show
    
type BinHeap a = [BinTree a]

rankZeroTree :: a -> BinTree a
rankZeroTree a = B 0 a []