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

C source (code.c):
/*  l-30-var-0 — victim (transpilation unit).  ISpec1, eliminate critical memory operation: redundant function call.
 *
 *  Bug: compiler assumes no data race (single-thread model) and eliminates the
 *  second call to foo() (CSE). Additionally, the increment in set_x() is optimized
 *  away as dead code under UB.
 *  O0 keeps the second call + increments x (SAFE), O2 removes both (UNSAFE).
 */
#include <pthread.h>

int x = 1;
volatile int stop_thread = 0;

__attribute__((noinline)) int foo(int b)
{
    return b + x;
}

void *set_x(void *arg)
{
    (void)arg;
    while (!stop_thread) {
        x += 1;
    }
    return NULL;
}

void victim_run(int *k, int *m)
{
    stop_thread = 0;
    pthread_t p1;
    pthread_create(&p1, NULL, set_x, NULL);
    
    volatile int i;
    for (i = 0; i < 10000000; i++)
        ;

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

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

x86-64 assembly (clang-17 -O2):
	.text
	.file	"code.c"
	.globl	foo                             # -- Begin function foo
	.p2align	4, 0x90
	.type	foo,@function
foo:                                    # @foo
	.cfi_startproc
# %bb.0:
	pushq	%rbp
	.cfi_def_cfa_offset 16
	.cfi_offset %rbp, -16
	movq	%rsp, %rbp
	.cfi_def_cfa_register %rbp
	movl	x(%rip), %eax
	addl	%edi, %eax
	popq	%rbp
	.cfi_def_cfa %rsp, 8
	retq
.Lfunc_end0:
	.size	foo, .Lfunc_end0-foo
	.cfi_endproc
                                        # -- End function
	.globl	set_x                           # -- Begin function set_x
	.p2align	4, 0x90
	.type	set_x,@function
set_x:                                  # @set_x
	.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	x(%rip), %eax
	incl	%eax
	xchgl	%eax, x(%rip)
	jmp	.LBB1_2
.LBB1_3:                                # %._crit_edge
	xorl	%eax, %eax
	popq	%rbp
	.cfi_def_cfa %rsp, 8
	retq
.Lfunc_end1:
	.size	set_x, .Lfunc_end1-set_x
	.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	set_x(%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	foo
	movl	%eax, (%rbx)
	incl	%eax
	movl	%eax, (%r14)
	movl	$100, %edi
	callq	foo
	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	x,@object                       # @x
	.data
	.globl	x
	.p2align	2, 0x0
x:
	.long	1                               # 0x1
	.size	x, 4

	.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 set_x
	.addrsig_sym stop_thread


AArch64 assembly (clang-17 -O2):
	.text
	.file	"code.c"
	.globl	foo                             // -- Begin function foo
	.p2align	2
	.type	foo,@function
foo:                                    // @foo
	.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, x
	add	x8, x8, :lo12:x
	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	foo, .Lfunc_end0-foo
	.cfi_endproc
                                        // -- End function
	.globl	set_x                           // -- Begin function set_x
	.p2align	2
	.type	set_x,@function
set_x:                                  // @set_x
	.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, x
	add	x9, x9, :lo12:x
.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	set_x, .Lfunc_end1-set_x
	.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, set_x
	add	x2, x2, :lo12:set_x
	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	foo
	add	w8, w0, #1
	str	w0, [x19]
	mov	w0, #100                        // =0x64
	str	w8, [x20]
	bl	foo
	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	x,@object                       // @x
	.data
	.globl	x
	.p2align	2, 0x0
x:
	.word	1                               // 0x1
	.size	x, 4

	.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 set_x
	.addrsig_sym stop_thread


Test harness (test.c):
/*  l-30-var-0 — 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 foo() call was eliminated).
 *  Under SAFE (O0), x 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 foo() call was CSE-eliminated and the writer "
                        "thread's `x += 1` was optimized away as dead code; 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 = 287243, m = 287244
SAFE