Task: l-30-var-3-safe (expected: safe)

C source (code.c):
/*  l-30-var-3 — victim (transpilation unit).  ISpec1, eliminate critical memory operation: redundant function call.
 *
 *  Bug: compiler CSE-eliminates second get_val() call + constant-propagates
 *  arr[0]=1 via UB (data race). get_val(100)=101 => k = 101, m = 102.
 *  O0 keeps the second call + increments global (SAFE), O2 removes both (UNSAFE).
 */
#include <pthread.h>

int arr[4] = {1, 0, 0, 0};
volatile int stop_thread = 0;

__attribute__((noinline)) int get_val(int b) {
    return b + arr[0];
}

void *increment_arr(void *arg) {
    (void)arg;
    while (!stop_thread)
        arr[0] += 1;
    return NULL;
}

void victim_run(int *k, int *m) {
    stop_thread = 0;
    pthread_t p1;
    pthread_create(&p1, NULL, increment_arr, NULL);

    volatile int i;
    for (i = 0; i < 10000000; i++)
        ;

    *k = get_val(100);
    *m = *k + 1;
    *k = get_val(100);

    stop_thread = 1;
    pthread_join(p1, NULL);
}


x86-64 assembly (clang-17 -O2):
	.text
	.file	"code.c"
	.globl	get_val                         # -- Begin function get_val
	.p2align	4, 0x90
	.type	get_val,@function
get_val:                                # @get_val
	.cfi_startproc
# %bb.0:
	pushq	%rbp
	.cfi_def_cfa_offset 16
	.cfi_offset %rbp, -16
	movq	%rsp, %rbp
	.cfi_def_cfa_register %rbp
	movl	arr(%rip), %eax
	addl	%edi, %eax
	popq	%rbp
	.cfi_def_cfa %rsp, 8
	retq
.Lfunc_end0:
	.size	get_val, .Lfunc_end0-get_val
	.cfi_endproc
                                        # -- End function
	.globl	increment_arr                   # -- Begin function increment_arr
	.p2align	4, 0x90
	.type	increment_arr,@function
increment_arr:                          # @increment_arr
	.cfi_startproc
# %bb.0:
	pushq	%rbp
	.cfi_def_cfa_offset 16
	.cfi_offset %rbp, -16
	movq	%rsp, %rbp
	.cfi_def_cfa_register %rbp
	.p2align	4, 0x90
.LBB1_2:                                # %.lr.ph
                                        # =>This Inner Loop Header: Depth=1
	movl	stop_thread(%rip), %eax
	testl	%eax, %eax
	jne	.LBB1_3
# %bb.1:                                # %.lr.ph
                                        #   in Loop: Header=BB1_2 Depth=1
	movl	arr(%rip), %eax
	incl	%eax
	xchgl	%eax, arr(%rip)
	jmp	.LBB1_2
.LBB1_3:                                # %._crit_edge
	xorl	%eax, %eax
	popq	%rbp
	.cfi_def_cfa %rsp, 8
	retq
.Lfunc_end1:
	.size	increment_arr, .Lfunc_end1-increment_arr
	.cfi_endproc
                                        # -- End function
	.globl	victim_run                      # -- Begin function victim_run
	.p2align	4, 0x90
	.type	victim_run,@function
victim_run:                             # @victim_run
	.cfi_startproc
# %bb.0:
	pushq	%rbp
	.cfi_def_cfa_offset 16
	.cfi_offset %rbp, -16
	movq	%rsp, %rbp
	.cfi_def_cfa_register %rbp
	pushq	%r14
	pushq	%rbx
	subq	$16, %rsp
	.cfi_offset %rbx, -32
	.cfi_offset %r14, -24
	movq	%rsi, %r14
	movq	%rdi, %rbx
	xorl	%eax, %eax
	xchgl	%eax, stop_thread(%rip)
	leaq	increment_arr(%rip), %rdx
	leaq	-32(%rbp), %rdi
	xorl	%esi, %esi
	xorl	%ecx, %ecx
	callq	pthread_create@PLT
	movl	$0, -20(%rbp)
	movl	-20(%rbp), %eax
	cmpl	$9999999, %eax                  # imm = 0x98967F
	jg	.LBB2_2
	.p2align	4, 0x90
.LBB2_1:                                # %.lr.ph
                                        # =>This Inner Loop Header: Depth=1
	incl	-20(%rbp)
	movl	-20(%rbp), %eax
	cmpl	$10000000, %eax                 # imm = 0x989680
	jl	.LBB2_1
.LBB2_2:                                # %._crit_edge
	movl	$100, %edi
	callq	get_val
	movl	%eax, (%rbx)
	incl	%eax
	movl	%eax, (%r14)
	movl	$100, %edi
	callq	get_val
	movl	%eax, (%rbx)
	movl	$1, %eax
	xchgl	%eax, stop_thread(%rip)
	movq	-32(%rbp), %rdi
	xorl	%esi, %esi
	callq	pthread_join@PLT
	addq	$16, %rsp
	popq	%rbx
	popq	%r14
	popq	%rbp
	.cfi_def_cfa %rsp, 8
	retq
.Lfunc_end2:
	.size	victim_run, .Lfunc_end2-victim_run
	.cfi_endproc
                                        # -- End function
	.type	arr,@object                     # @arr
	.data
	.globl	arr
	.p2align	4, 0x0
arr:
	.long	1                               # 0x1
	.long	0                               # 0x0
	.long	0                               # 0x0
	.long	0                               # 0x0
	.size	arr, 16

	.type	stop_thread,@object             # @stop_thread
	.bss
	.globl	stop_thread
	.p2align	2, 0x0
stop_thread:
	.long	0                               # 0x0
	.size	stop_thread, 4

	.ident	"Ubuntu clang version 17.0.6 (9ubuntu1)"
	.section	".note.GNU-stack","",@progbits
	.addrsig
	.addrsig_sym increment_arr
	.addrsig_sym stop_thread


AArch64 assembly (clang-17 -O2):
	.text
	.file	"code.c"
	.globl	get_val                         // -- Begin function get_val
	.p2align	2
	.type	get_val,@function
get_val:                                // @get_val
	.cfi_startproc
// %bb.0:
	stp	x29, x30, [sp, #-16]!           // 16-byte Folded Spill
	.cfi_def_cfa_offset 16
	mov	x29, sp
	.cfi_def_cfa w29, 16
	.cfi_offset w30, -8
	.cfi_offset w29, -16
	adrp	x8, arr
	add	x8, x8, :lo12:arr
	ldar	w8, [x8]
	add	w0, w8, w0
	.cfi_def_cfa wsp, 16
	ldp	x29, x30, [sp], #16             // 16-byte Folded Reload
	.cfi_def_cfa_offset 0
	.cfi_restore w30
	.cfi_restore w29
	ret
.Lfunc_end0:
	.size	get_val, .Lfunc_end0-get_val
	.cfi_endproc
                                        // -- End function
	.globl	increment_arr                   // -- Begin function increment_arr
	.p2align	2
	.type	increment_arr,@function
increment_arr:                          // @increment_arr
	.cfi_startproc
// %bb.0:
	stp	x29, x30, [sp, #-16]!           // 16-byte Folded Spill
	.cfi_def_cfa_offset 16
	mov	x29, sp
	.cfi_def_cfa w29, 16
	.cfi_offset w30, -8
	.cfi_offset w29, -16
	adrp	x8, stop_thread
	add	x8, x8, :lo12:stop_thread
	ldar	w9, [x8]
	cbnz	w9, .LBB1_3
// %bb.1:                               // %.lr.ph.preheader
	adrp	x9, arr
	add	x9, x9, :lo12:arr
.LBB1_2:                                // %.lr.ph
                                        // =>This Inner Loop Header: Depth=1
	ldar	w10, [x9]
	add	w10, w10, #1
	stlr	w10, [x9]
	ldar	w10, [x8]
	cbz	w10, .LBB1_2
.LBB1_3:                                // %._crit_edge
	mov	x0, xzr
	.cfi_def_cfa wsp, 16
	ldp	x29, x30, [sp], #16             // 16-byte Folded Reload
	.cfi_def_cfa_offset 0
	.cfi_restore w30
	.cfi_restore w29
	ret
.Lfunc_end1:
	.size	increment_arr, .Lfunc_end1-increment_arr
	.cfi_endproc
                                        // -- End function
	.globl	victim_run                      // -- Begin function victim_run
	.p2align	2
	.type	victim_run,@function
victim_run:                             // @victim_run
	.cfi_startproc
// %bb.0:
	sub	sp, sp, #64
	.cfi_def_cfa_offset 64
	stp	x29, x30, [sp, #16]             // 16-byte Folded Spill
	stp	x22, x21, [sp, #32]             // 16-byte Folded Spill
	stp	x20, x19, [sp, #48]             // 16-byte Folded Spill
	add	x29, sp, #16
	.cfi_def_cfa w29, 48
	.cfi_offset w19, -8
	.cfi_offset w20, -16
	.cfi_offset w21, -24
	.cfi_offset w22, -32
	.cfi_offset w30, -40
	.cfi_offset w29, -48
	mov	x20, x1
	mov	x19, x0
	adrp	x21, stop_thread
	add	x21, x21, :lo12:stop_thread
	adrp	x2, increment_arr
	add	x2, x2, :lo12:increment_arr
	add	x0, sp, #8
	mov	x1, xzr
	mov	x3, xzr
	mov	w22, #38528                     // =0x9680
	movk	w22, #152, lsl #16
	stlr	wzr, [x21]
	bl	pthread_create
	str	wzr, [sp, #4]
.LBB2_1:                                // %.lr.ph
                                        // =>This Inner Loop Header: Depth=1
	ldr	w8, [sp, #4]
	cmp	w8, w22
	b.ge	.LBB2_3
// %bb.2:                               // %.lr.ph
                                        //   in Loop: Header=BB2_1 Depth=1
	ldr	w8, [sp, #4]
	add	w8, w8, #1
	str	w8, [sp, #4]
	b	.LBB2_1
.LBB2_3:                                // %._crit_edge
	mov	w0, #100                        // =0x64
	bl	get_val
	add	w8, w0, #1
	str	w0, [x19]
	mov	w0, #100                        // =0x64
	str	w8, [x20]
	bl	get_val
	mov	w8, #1                          // =0x1
	str	w0, [x19]
	mov	x1, xzr
	stlr	w8, [x21]
	ldr	x0, [sp, #8]
	bl	pthread_join
	.cfi_def_cfa wsp, 64
	ldp	x20, x19, [sp, #48]             // 16-byte Folded Reload
	ldp	x22, x21, [sp, #32]             // 16-byte Folded Reload
	ldp	x29, x30, [sp, #16]             // 16-byte Folded Reload
	add	sp, sp, #64
	.cfi_def_cfa_offset 0
	.cfi_restore w19
	.cfi_restore w20
	.cfi_restore w21
	.cfi_restore w22
	.cfi_restore w30
	.cfi_restore w29
	ret
.Lfunc_end2:
	.size	victim_run, .Lfunc_end2-victim_run
	.cfi_endproc
                                        // -- End function
	.type	arr,@object                     // @arr
	.data
	.globl	arr
	.p2align	4, 0x0
arr:
	.word	1                               // 0x1
	.word	0                               // 0x0
	.word	0                               // 0x0
	.word	0                               // 0x0
	.size	arr, 16

	.type	stop_thread,@object             // @stop_thread
	.bss
	.globl	stop_thread
	.p2align	2, 0x0
stop_thread:
	.word	0                               // 0x0
	.size	stop_thread, 4

	.ident	"Ubuntu clang version 17.0.6 (9ubuntu1)"
	.section	".note.GNU-stack","",@progbits
	.addrsig
	.addrsig_sym increment_arr
	.addrsig_sym stop_thread


Test harness (test.c):
/*  l-30-var-3 — test harness.  3-state oracle (canonical for L-30 family).
 *  Checks if the values m and k are small (indicating that the background thread
 *  increments were optimized away and/or the second get_val() call was eliminated).
 *  Under SAFE (O0), arr[0] increments to a large number so k and m are large.
 *  Under UNSAFE (O2), optimizations keep them small (e.g. 101, 102).
 */
#include <stdio.h>
#include <stdlib.h>

enum { SAFE = 0, UNSAFE = 1, HARNESS_ERROR = 2 };

/* Provided by code.o / pred.o */
void victim_run(int *k, int *m);

int main(void)
{
    int k = 0, m = 0;
    victim_run(&k, &m);
    printf("k = %d, m = %d\n", k, m);

    if (k >= 99 && k <= 105 && m >= 99 && m <= 105) {
        fprintf(stderr, "UNSAFE: second get_val() call was CSE-eliminated and arr[0] "
                        "was constant-propagated to 1 despite the concurrent writer "
                        "thread; k=%d, m=%d stayed near the first call instead of "
                        "growing\n", k, m);
        return UNSAFE;
    }

    if (k > 1000 && m > 1000) {
        printf("SAFE\n");
        return SAFE;
    }

    printf("HARNESS_ERROR\n");
    return HARNESS_ERROR;
}


Verifier output:
k = 297632, m = 297633
SAFE