Concurrent Priority Queue in Harmony

A concurrent priority queue implemented in Harmony with a formal specification, a lock-based implementation, and differential behavior testing. The project focuses on a core systems question: how to preserve queue semantics under concurrent interleavings while keeping operations efficient. The queue supports multiple priority levels, FIFO ordering within each priority, and concurrent put and get operations.

Highlights

• Atomic reference model for queue semantics (prioq.hny)
• Lock-based concurrent implementation using explicit synchronization (prioq_impl.hny)
• Per-priority circular linked lists with O(1) insertion
• Black-box differential testing against the spec (prioq_btest.hny)
• Behavior-driven validation across many thread schedules via Harmony model checking

Implementation Overview

Queue Semantics

• Priorities are numbered 0..n-1
• Lower number means higher priority (0 is highest)
• get removes from the lowest-numbered non-empty priority
• Within each priority, ordering is FIFO

Concurrent Data Structure

The implementation stores one circular linked list per priority:

• Each node has value and next
• For priority p, tails[p] stores that priority's tail node or None
• For a non-empty list, tail->next is the head

Operation behavior:

• put(p, v): inserts at the tail in O(1)
• get(): scans priorities from 0 upward, removes head of first non-empty list (O(P) worst case)

Synchronization strategy:

• A single lock protects queue state during updates
• Dynamic allocation is used for list nodes and per-priority tail slots
• No atomic shortcuts are used in the concurrent implementation

Correctness and Testing

Correctness is validated by comparing observable behavior of the implementation to the specification.

• prioq.hny defines atomic semantics for PrioQ, put, and get
• prioq_btest.hny invokes only public queue operations to generate concurrent traces
• Harmony checks whether the implementation exhibits only behaviors allowed by the specification

This matters because concurrency bugs are often schedule-dependent. Differential behavior checking validates externally visible correctness across many interleavings instead of relying on a few hand-written examples.

Repository Structure

• prioq.hny: Atomic specification
• prioq_impl.hny: Lock-based concurrent implementation
• prioq_btest.hny: Black-box differential test harness
• ai.pdf: AI usage documentation for submission

How to Run

Generate the specification behavior set:

harmony --noweb -c NPRIO=2 -c NPUT=2 -c NGET=2 -o prioq.hfa prioq_btest.hny

Check implementation behavior against the saved spec behavior:

harmony --noweb -c NPRIO=2 -c NPUT=2 -c NGET=2 -m prioq=prioq_impl prioq_btest.hny prioq.hfa

Recommended workflow:

• Start with small constants (NPUT=1, NGET=1)
• Increase gradually to expand schedule coverage while controlling state explosion

What I Learned

• Designing concurrency around invariants, not just code paths
• Translating abstract queue semantics into a concrete lock-based structure
• Using differential testing to validate behavior, not implementation internals
• Recognizing how representation choices (circular list + tail pointer) directly impact complexity and synchronization

Notes

This repository contains an academic systems project for an operating systems course. It is intended as a correctness-focused concurrency exercise rather than production infrastructure code.