Documentation

Start Here

The Harmony Online Textbook

A Comprehensive Introduction to Concurrent Programming
Download the PDF Version

Installing Harmony

A Quick Start Guide

Language Reference

Language features and syntax

Module Reference

Convenient and written in Harmony

Community

Join GitHub Discussions on Harmony

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.

Read more

Downloads

Requires Python 3.8+

Harmony on Command Line

  • Standalone model checking
  • State machine output
  • Interactive HTML output
  • Installation using pip
Install

HarmonyLang for VSCode

  • Syntax Highlighting
  • Intelligent Code Completion
  • In-editor Visualizer
  • Automatic Installation
Download

Open Source on GitHub

  • Full sources
  • Parser in Antlr
  • Fast model checker in C
  • Integrated into Python module
Download

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.

Bounded Buffer

A solution to the producer/consumer problem using a Hoare monitor.

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.

2-Lock Concurrent Queue

This queue implementation uses separate locks for the head and the tail.

Paxos

A way for multiple distributed processes to come to agreement, even in the face of failures.

Educators

Educator Resources

Concurrent programming is hard to teach. 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.

Slide Set (PowerPoint) Homework and Autograding Example Exam Questions

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 Interface

Contact

Contact Us