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

C source (code.c):
/*  l-30-var-2 — 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 get_token() (CSE) across a never-taken conditional branch.
 *  Additionally, the increment in rotate_token() is optimized away as dead code under UB.
 *  O0 keeps the second call + increments global (SAFE), O2 removes both (UNSAFE).
 */
#include <pthread.h>

int token = 1;
volatile int stop_thread = 0;

__attribute__((noinline)) int get_token(int base) {
    return base + token;
}

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

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

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

    int flag = 0;
    *k = get_token(100);
    *m = *k + 1;
    if (flag) {          /* never taken, but present between the two calls */
        stop_thread = 1;
        pthread_join(p1, NULL);
        return;
    }
    *k = get_token(100);  /* second call eliminated by compiler */

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


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


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


Test harness (test.c):
/*  l-30-var-2 — test harness.  3-state oracle (canonical: see 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 get_token() call was eliminated).
 *  Under SAFE (O0), token 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_token() call (across a never-taken branch) "
                        "was CSE-eliminated and the writer thread's `token += 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 = 289533, m = 289534
SAFE