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

C source (code.c):
/*  l-30-var-4 — victim (transpilation unit).  ISpec1, eliminate critical memory operation: redundant function call.
 *
 *  Bug: compiler assumes no data race (single-thread model) and CSE-eliminates the
 *  second compute() call and constant-propagates counter=1LL via UB (data race).
 *  O0 keeps the second call + increments global counter (SAFE), O2 removes both (UNSAFE).
 */
#include <pthread.h>

long long counter = 1LL;
volatile int stop_thread = 0;

__attribute__((noinline)) int compute(int b) {
    return (int)(b + counter);
}

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

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

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

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

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


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

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


AArch64 assembly (clang-17 -O2):
	.text
	.file	"code.c"
	.globl	compute                         // -- Begin function compute
	.p2align	2
	.type	compute,@function
compute:                                // @compute
	.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, counter
	add	x8, x8, :lo12:counter
	ldar	x8, [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	compute, .Lfunc_end0-compute
	.cfi_endproc
                                        // -- End function
	.globl	increment_counter               // -- Begin function increment_counter
	.p2align	2
	.type	increment_counter,@function
increment_counter:                      // @increment_counter
	.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, counter
	add	x9, x9, :lo12:counter
.LBB1_2:                                // %.lr.ph
                                        // =>This Inner Loop Header: Depth=1
	ldar	x10, [x9]
	add	x10, x10, #1
	stlr	x10, [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_counter, .Lfunc_end1-increment_counter
	.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_counter
	add	x2, x2, :lo12:increment_counter
	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	compute
	add	w8, w0, #1
	str	w0, [x19]
	mov	w0, #100                        // =0x64
	str	w8, [x20]
	bl	compute
	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	counter,@object                 // @counter
	.data
	.globl	counter
	.p2align	3, 0x0
counter:
	.xword	1                               // 0x1
	.size	counter, 8

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


Test harness (test.c):
/*  l-30-var-4 — test harness.  3-state oracle (referring to l-30-var-0/test.c as canonical).
 *  Checks if the values m and k are small (indicating that the background thread
 *  increments were optimized away and/or the second compute() call was eliminated).
 *  Under SAFE (O0), counter 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 compute() call was CSE-eliminated and counter "
                        "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 = 293321, m = 293322
SAFE