This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | @article{10.1145/3689727, | |
| author = {Geeson, Luke and Brotherston, James and Dijkstra, Wilco and Donaldson, Alastair F. and Smith, Lee and Sorensen, Tyler and Wickerson, John}, | |
| title = {Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations}, | |
| year = {2024}, | |
| issue_date = {October 2024}, | |
| publisher = {Association for Computing Machinery}, | |
| address = {New York, NY, USA}, | |
| volume = {8}, | |
| number = {OOPSLA2}, | |
| url = {https://doi.org/10.1145/3689727}, | 
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | @INPROCEEDINGS{GeesonSmithCGO24, | |
| author={Geeson, Luke and Smith, Lee}, | |
| booktitle={2024 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)}, | |
| title={{C}ompiler {T}esting with {R}elaxed {M}emory {M}odels}, | |
| year={2024}, | |
| month={Mar}, | |
| volume={}, | |
| number={}, | |
| pages={334-348}, | |
| isbn={979-8-3503-9509-9}, | 
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | @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)}, | 
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | 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; | 
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | { [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] ; | 
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | { [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] ; | 
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | { *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); | 
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | 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 = ' ' | 
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | 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 | 
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
  | 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 | 
NewerOlder