# Introduction

Harmony is a Python-like programming language for testing and experimenting with concurrent programs. Instead of "running" code, Harmony programs are model-checked so that all corner cases are explored. If there is a problem, Harmony provides a short but detailed example of an execution that leads to the problem.

Here is Peterson's Algorithm in Harmony, along with code to verify mutual exclusion:

peterson.hny
sequential flags, turn

flags = [ False, False ]
turn = choose({0, 1})

while choose({ False, True }):
# Enter critical section
flags[self] = True
turn = 1 - self
await (not flags[1 - self]) or (turn == self)

# Critical section is here
cs: assert countLabel(cs) == 1

# Leave critical section
flags[self] = False