Bringing the Flexible Multiprocessor Locking Protocol (FMLP) into the strict RTEMS 7 SMP SuperCore requires rigorous proof. It is not enough that the logic works; we have to mathematically prove it behaves identically to the academic theorems.

FMLP uses two variants for handling resource sharing: FMLP-Short (FMLP-S) for fast spinlocks, and FMLP-Long (FMLP-L) for suspension and priority inheritance.

I created three dedicated SMP test suites to prove the implementation.

The Long Variant: spfmlp01

The first suite focuses on the suspension-based FMLP-Long variant.

I forced priority contention across different SMP cores. When a low-priority task holds an FMLP-L lock and a high-priority task attempts to acquire it, the low-priority task must magically “inherit” the high priority to finish quickly.

  • Priority Inheritance: Successfully elevates the blocker.
  • Mutual Exclusion: Safely releases the resource, preventing unbounded priority inversion.

The Short Variant: spfmlp02

The spfmlp02 test shifts to the fast, non-preemptive busy-waiting of FMLP-Short.

Once a task acquires an FMLP-S lock, it essentially disables preemptive scheduling for its local processor until the lock is released. You can’t misuse the SuperCore and get away with it.

I forced multiple tasks on a single core to fiercely contend for the same lock, tracking the exact tick boundaries to ensure the executing thread successfully suppresses preemptions.

The Complex Case: spfmlp03

The final test tackles the most mathematically rigorous characteristics of FMLP-Short: strict FIFO ordering and the Priority Ceiling Protocol.

This was the most complex scenario, where tasks of identical and differing priorities slam into a single FMLP-S lock simultaneously:

  • FIFO Ordering: Tasks are serviced strictly First-In-First-Out, ignoring their base priority.
  • Priority Ceiling: Priority inversion is neutralized by immediately raising the lock holder to a predefined ceiling.

The Result

Porting FMLP wasn’t just about translating a research paper into C code. By writing spfmlp01, spfmlp02, and spfmlp03, we now have automated, deterministic proof that the RTEMS SuperCore architecture correctly enforces these protocols.