State search for the three-round cross-CTA example

Pseudocode · three rounds

        if cta == 1:  # producer
          for round in range(3):
            arrive_remote(full)
        if cta == 0:  # consumer
          for round in range(3):
            wait(full, round % 2)
            out[round] = round + 1
      

One thread per CTA executes the protocol. Barrier full lives on CTA 0 and needs one arrival per phase. Initialization is complete.

State
P = producer arrivals
C = completed consumer waits
Each arrival advances the phase; parity = phase % 2.

The search stops a branch when the producer completes a second phase before the consumer observes the first.

Reachable states · L = pseudocode line

Try each enabled event

After either of the first two arrivals, the consumer can finish its wait or the producer can arrive again. The search explores both choices. Red states mark a phase completed before the preceding phase was observed.

Try each enabled event

All three rounds complete

The second arrival overtakes the first wait