About
What is Harmony?
Concurrent programming is hard to get right. A deadlock might occur only once in a million executions, caused by the most esoteric of circumstances. Harmony makes finding those bugs easy.
- Checks every possible interleaving of processes
- Detects non-compilance with invariants
- Provides the shortest path to a failing execution
Learning programming in Harmony should be straightforward to those familiar with Python or similar languages. In addition to our online documentation, we provide a free textbook with many programming examples including Peterson's Algorithm, Dining Philosophers, Producer/Consumer queues, and barrier synchronization.
Online textbook PDF textbook Language Reference Module Reference Educator ResourcesDownloads
Harmony on Command Line
- Standalone model checking
- State machine output
- Interactive HTML output
- Installation using pip
HarmonyLang for VSCode
- Syntax Highlighting
- Intelligent Code Completion
- In-editor Visualizer
- Automatic Installation
Examples
Try out Harmony
Dining Philosophers
Formulated in 1965 by Edsger Dijkstra as a student exam exercise, presented in terms of computers competing for access to tape drive peripherals.
Peterson's Algorithm
An algorithm for mutual exclusion that allows two or more processes to share a single-use resource without conflict, using only shared memory for communication.
Reader/Writer Problem
We want to prevent more than one thread modifying the shared resource simultaneously and allow for two or more readers to access the shared resource for reading at the same time.
Educators
Educator Resources
Harmony has been used to teach concurrent programming at Cornell since 2020 by Robbert van Renesse and by Lorenzo Alvisi. Harmony comes with educational materials, including a free textbook (both online and PDF) with exercises, a slide set, example homework assignments, and example exam questions (answers available upon request). Also, the Harmony model checker makes it relatively easy to auto-grade student programs.
- Learning curve appropriate for undergraduate level
- Requires no background in formal methods
- Extensive educational materials
- Supports autograding
Harmony allows both specification and implementation of concurrent programs, and checks implementations automatically against specifications. Harmony runs on Linux, Mac OS X, and Windows. Harmony can be used on the command line (simplifying autograding) or within VSCode.
Team
Our Primary Contributors

Robbert van Renesse
Creator of the Harmony Project
Anthony Yang
Compilers & Data Output
Kevin Sun
Design & Documentation
Haobin Ni
Design
William Ma
Compilers & Visualization
Renyu Li
Graphical User InterfaceContact
Contact Us
Email:
rvr@cs.cornell.edu