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

C source (code.c):
/*  l-30-var-5 — victim (transpilation unit).  ISpec1, eliminate critical memory operation: redundant function call.
 *
 *  Bug: compiler CSE-eliminates second validate() call inside run_check() (CSE) because
 *  the global variable version is assumed to be invariant. Additionally, the increment
 *  in bump_version() is optimized away as dead code under UB.
 *  O0 keeps the second call + increments global (SAFE), O2 removes both (UNSAFE).
 */
#include <pthread.h>

int version = 1;
volatile int stop_thread = 0;

__attribute__((noinline)) int validate(int id) {
    return id + version;
}

__attribute__((noinline)) void run_check(int id, int *k, int *m) {
    *k = validate(id);
    *m = *k + 1;
    *k = validate(id);   /* second call eliminated by compiler */
}

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

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

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

    run_check(100, k, m);

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


x86-64 assembly (clang-17 -O2):
	.text
	.file	"code.c"
	.globl	validate                        # -- Begin function validate
	.p2align	4, 0x90
	.type	validate,@function
validate:                               # @validate
	.cfi_startproc
# %bb.0:
	pushq	%rbp
	.cfi_def_cfa_offset 16
	.cfi_offset %rbp, -16
	movq	%rsp, %rbp
	.cfi_def_cfa_register %rbp
	movl	version(%rip), %eax
	addl	%edi, %eax
	popq	%rbp
	.cfi_def_cfa %rsp, 8
	retq
.Lfunc_end0:
	.size	validate, .Lfunc_end0-validate
	.cfi_endproc
                                        # -- End function
	.globl	run_check                       # -- Begin function run_check
	.p2align	4, 0x90
	.type	run_check,@function
run_check:                              # @run_check
	.cfi_startproc
# %bb.0:
	pushq	%rbp
	.cfi_def_cfa_offset 16
	.cfi_offset %rbp, -16
	movq	%rsp, %rbp
	.cfi_def_cfa_register %rbp
	pushq	%r15
	pushq	%r14
	pushq	%rbx
	pushq	%rax
	.cfi_offset %rbx, -40
	.cfi_offset %r14, -32
	.cfi_offset %r15, -24
	movq	%rdx, %rbx
	movq	%rsi, %r14
	movl	%edi, %r15d
	callq	validate
	movl	%eax, (%r14)
	incl	%eax
	movl	%eax, (%rbx)
	movl	%r15d, %edi
	callq	validate
	movl	%eax, (%r14)
	addq	$8, %rsp
	popq	%rbx
	popq	%r14
	popq	%r15
	popq	%rbp
	.cfi_def_cfa %rsp, 8
	retq
.Lfunc_end1:
	.size	run_check, .Lfunc_end1-run_check
	.cfi_endproc
                                        # -- End function
	.globl	bump_version                    # -- Begin function bump_version
	.p2align	4, 0x90
	.type	bump_version,@function
bump_version:                           # @bump_version
	.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
.LBB2_2:                                # %.lr.ph
                                        # =>This Inner Loop Header: Depth=1
	movl	stop_thread(%rip), %eax
	testl	%eax, %eax
	jne	.LBB2_3
# %bb.1:                                # %.lr.ph
                                        #   in Loop: Header=BB2_2 Depth=1
	movl	version(%rip), %eax
	incl	%eax
	xchgl	%eax, version(%rip)
	jmp	.LBB2_2
.LBB2_3:                                # %._crit_edge
	xorl	%eax, %eax
	popq	%rbp
	.cfi_def_cfa %rsp, 8
	retq
.Lfunc_end2:
	.size	bump_version, .Lfunc_end2-bump_version
	.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, %rbx
	movq	%rdi, %r14
	xorl	%eax, %eax
	xchgl	%eax, stop_thread(%rip)
	leaq	bump_version(%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	.LBB3_2
	.p2align	4, 0x90
.LBB3_1:                                # %.lr.ph
                                        # =>This Inner Loop Header: Depth=1
	incl	-20(%rbp)
	movl	-20(%rbp), %eax
	cmpl	$10000000, %eax                 # imm = 0x989680
	jl	.LBB3_1
.LBB3_2:                                # %._crit_edge
	movl	$100, %edi
	movq	%r14, %rsi
	movq	%rbx, %rdx
	callq	run_check
	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_end3:
	.size	victim_run, .Lfunc_end3-victim_run
	.cfi_endproc
                                        # -- End function
	.type	version,@object                 # @version
	.data
	.globl	version
	.p2align	2, 0x0
version:
	.long	1                               # 0x1
	.size	version, 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 bump_version
	.addrsig_sym stop_thread


AArch64 assembly (clang-17 -O2):
	.text
	.file	"code.c"
	.globl	validate                        // -- Begin function validate
	.p2align	2
	.type	validate,@function
validate:                               // @validate
	.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, version
	add	x8, x8, :lo12:version
	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	validate, .Lfunc_end0-validate
	.cfi_endproc
                                        // -- End function
	.globl	run_check                       // -- Begin function run_check
	.p2align	2
	.type	run_check,@function
run_check:                              // @run_check
	.cfi_startproc
// %bb.0:
	stp	x29, x30, [sp, #-48]!           // 16-byte Folded Spill
	.cfi_def_cfa_offset 48
	str	x21, [sp, #16]                  // 8-byte Folded Spill
	stp	x20, x19, [sp, #32]             // 16-byte Folded Spill
	mov	x29, sp
	.cfi_def_cfa w29, 48
	.cfi_offset w19, -8
	.cfi_offset w20, -16
	.cfi_offset w21, -32
	.cfi_offset w30, -40
	.cfi_offset w29, -48
	mov	x19, x2
	mov	x20, x1
	mov	w21, w0
	bl	validate
	add	w8, w0, #1
	str	w0, [x20]
	mov	w0, w21
	str	w8, [x19]
	bl	validate
	str	w0, [x20]
	.cfi_def_cfa wsp, 48
	ldp	x20, x19, [sp, #32]             // 16-byte Folded Reload
	ldr	x21, [sp, #16]                  // 8-byte Folded Reload
	ldp	x29, x30, [sp], #48             // 16-byte Folded Reload
	.cfi_def_cfa_offset 0
	.cfi_restore w19
	.cfi_restore w20
	.cfi_restore w21
	.cfi_restore w30
	.cfi_restore w29
	ret
.Lfunc_end1:
	.size	run_check, .Lfunc_end1-run_check
	.cfi_endproc
                                        // -- End function
	.globl	bump_version                    // -- Begin function bump_version
	.p2align	2
	.type	bump_version,@function
bump_version:                           // @bump_version
	.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, .LBB2_3
// %bb.1:                               // %.lr.ph.preheader
	adrp	x9, version
	add	x9, x9, :lo12:version
.LBB2_2:                                // %.lr.ph
                                        // =>This Inner Loop Header: Depth=1
	ldar	w10, [x9]
	add	w10, w10, #1
	stlr	w10, [x9]
	ldar	w10, [x8]
	cbz	w10, .LBB2_2
.LBB2_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_end2:
	.size	bump_version, .Lfunc_end2-bump_version
	.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	x19, x1
	mov	x20, x0
	adrp	x21, stop_thread
	add	x21, x21, :lo12:stop_thread
	adrp	x2, bump_version
	add	x2, x2, :lo12:bump_version
	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]
.LBB3_1:                                // %.lr.ph
                                        // =>This Inner Loop Header: Depth=1
	ldr	w8, [sp, #4]
	cmp	w8, w22
	b.ge	.LBB3_3
// %bb.2:                               // %.lr.ph
                                        //   in Loop: Header=BB3_1 Depth=1
	ldr	w8, [sp, #4]
	add	w8, w8, #1
	str	w8, [sp, #4]
	b	.LBB3_1
.LBB3_3:                                // %._crit_edge
	mov	w0, #100                        // =0x64
	mov	x1, x20
	mov	x2, x19
	bl	run_check
	mov	w8, #1                          // =0x1
	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_end3:
	.size	victim_run, .Lfunc_end3-victim_run
	.cfi_endproc
                                        // -- End function
	.type	version,@object                 // @version
	.data
	.globl	version
	.p2align	2, 0x0
version:
	.word	1                               // 0x1
	.size	version, 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 bump_version
	.addrsig_sym stop_thread


Test harness (test.c):
/*  l-30-var-5 — test harness.  3-state oracle (canonical structure in l-30-var-0/test.c).
 *  Checks if the values m and k are small (indicating that the background thread
 *  increments were optimized away and/or the second validate() call was eliminated).
 *  Under SAFE (O0), version 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 validate() call inside run_check() was "
                        "CSE-eliminated and the writer thread's `version += 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 = 285741, m = 285742
SAFE