README.md — Starvation and Liveness in an RTIC-Style Queue Model (TLA+)

This repository models RTIC-style priority scheduling and starvation behavior using PlusCal/TLA+.

The system contains three tasks with explicit fixed priorities:

ISR — highest‑priority periodic producer
Consumer — medium priority (in updated Option B)
Logger — lowest priority CPU burner

This updated Option‑B model demonstrates:

How scheduler priority ordering affects starvation
Why Consumer starvation disappears when its priority is raised
How liveness (ConsumerNotStarved) depends on both scheduling and fairness
Why the algorithm must NOT be fair in Option B
How to use an explicit fair scheduler to model NVIC‑like dispatch

1. Queue Model Overview

Shared variables:

qLen: queue length
QUEUE_CAP: queue capacity

Processes:

ISR: increments qLen
Consumer: decrements qLen, toggles consTick
Logger: toggles busy, burns CPU cycles

Only the Consumer participates in liveness checking via consTick.

2. Making the Model Finite-State

To keep the state space finite (required for TLC liveness checking):

busy := 1 - busy

rather than:

busy := busy + 1

3. Heartbeat for Consumer Execution

Consumer toggles a heartbeat:

consTick := 1 - consTick;

If Consumer is starved, consTick becomes constant.

4. Liveness Property — Detecting Consumer Starvation

ConsumerNotStarved ==
  /\ []<>(consTick = 0)
  /\ []<>(consTick = 1)

This requires:

Consumer must eventually reach both 0 and 1 infinitely often
Therefore Consumer must run infinitely often

If Consumer stops running → property is violated.

5. Option A — Implicit Scheduling

PlusCal’s built‑in interleaving controls execution order
Algorithm may be declared --fair
Starvation depends on per‑process fairness

6. Option B — Explicit Scheduler (Algorithm NOT Fair)

Option B replaces PlusCal’s default interleaving with a hardware‑like priority scheduler.

Algorithm must NOT be declared fair, because:

Fair algorithms override explicit scheduler behavior
We want scheduler‑controlled execution, not PlusCal‑imposed fairness

Only the Scheduler is declared fair.

7. Updated Option‑B Scheduler — Priority: ISR > Consumer > Logger

This version fixes the priority chain so that Consumer is no longer starved.

fair process Scheduler = SCHE_ID
variable
  isrEnabled,
  consEnabled,
  logEnabled;
begin SchedLoop:

  \* Who is enabled right now?
  isrEnabled  := qLen < QUEUE_CAP;   \* ISR can still produce
  consEnabled := qLen > 0;           \* Consumer can run if backlog exists
  logEnabled  := TRUE;               \* Logger always "ready"

  \* Priority: ISR > Consumer > Logger
  if isrEnabled then
    who := ISR_ID;
  elsif consEnabled then
    who := CONS_ID;
  elsif logEnabled then
    who := LOG_ID;
  else
    who := 0;                        \* idle
  end if;

  goto SchedLoop;
end process;

Why this removes starvation:

Whenever backlog exists (qLen > 0), Consumer is enabled
Consumer has higher priority than Logger
Consumer is declared fair, and now fairness is not vacuous because Consumer is enabled infinitely often
TLC guarantees Consumer runs infinitely often
consTick toggles infinitely often
ConsumerNotStarved holds—no violation is reported

This behavior matches a corrected RTIC configuration where Consumer’s priority is raised.

8. Priority Chain Diagram

 +------------------+      +-------------------+      +------------------+
 |     ISR_ID       | ---> |    CONS_ID        | ---> |     LOG_ID       |
 |  Highest Pri     |      |  Medium Pri       |      |  Lowest Pri      |
 +------------------+      +-------------------+      +------------------+

Scheduler always selects the leftmost enabled task.

9. Starvation-Free Timeline Example

Time ----->
who = ISR   ISR   CONS   ISR   CONS   CONS   ISR   CONS   ...
qLen:        1     2      1     2      1      3     2      ...
consTick:    0     0      1     1      0      1     1      0

Consumer runs infinitely often → consTick toggles → no starvation

10. Fairness Summary (Updated)

Component	Fair?	Reason
Algorithm	❌ No	Explicit scheduler controls dispatch
Scheduler	✔ Yes	Hardware-like dispatcher must always run
ISR	✔ Yes	Periodic interrupt guaranteed by hardware
Consumer	✔ Yes	Enabled when qLen > 0 → fairness ensures infinite runs
Logger	Optional	Lowest priority; may run only when others idle

Result:
With priority ISR > Consumer > Logger, starvation disappears.

End of README

wang32/LEDTIM2TIM3_TLA_OptB_v2

About

Resources

Uh oh!

Stars

Watchers

Forks

Releases

Languages