Harmony Language Details

Value Types and Operators

Chapter 4 provides an introduction to Harmony values Below is a complete list of Harmony value types with examples:

Type	Name	Example
Boolean	"bool"	`False`, `True`
Integer	"int"	..., --2, --1, 0, 1, 2, ...
String	"str"	`"`example`"`, .example
Program Counter	"pc"	((method names, lambdas, and labels)
List	"list"	[ 1, 2, 3, ], ( (1, 2), 3 ), [1,], ()
Dictionary	"dict"	{ .account: 12345, .valid: `False` }, {:}
Set	"set"	{}, { 1, 2, 3 }, { `False`, .id, 3 }
Address	"address"	?lock, ?flags[2], `None`
Context	"context"	(generated by stop or save expression)

In Harmony, there is no distinction between tuples (denoted with parentheses) and lists (denoted by square brackets). That is, their format is either (e, e, ..., e,) or [e, e, ..., e,]. They map indexes (starting at 0) to Harmony values. If the list has two or more elements, then the final comma is optional.

Method type e returns the type name of e.

All Harmony values are ordered with respect to one another. First they are ordered by type according to the table above. So, for example, True \(<\) 0 \(<\) .xyz \(<\) { 0 }. Within types, the following rules apply:

False \(<\) True;
integers are ordered in the natural way;
strings are lexicographically ordered;
program counters are ordered by their integer values;
lists are lexicographically ordered;
dictionaries are first converted into a list of ordered (key, value) pairs. Then two dictionaries are lexicographically ordered by this representation;
a set is first converted into an ordered list, then lexicographically ordered;
Except for None, an address is a pair of a function a list of arguments. Addresses are lexicographically ordered accordingly. None is the smallest address.
contexts are ordered deterministically in an unspecified way.

Harmony supports the following comparison operators:


e == e	equivalence
e != e	inequivalence
e \(<\) e, e \(<=\) e, e \(>\) e, e \(>=\) e	comparison

Comparison operators can be chained: x <= y == z means x <= y and y == z, although y is evaluated once in the former and twice in the latter expression.

Harmony supports atomic expression evaluation using the following syntax: atomically e, where e is some expression.

Boolean

The boolean type has only two possible values: False and True. Unlike Python, in Harmony booleans are distinct from integers, and in particular \(\mathbf{False} < 0\). In statements and expressions where booleans are expected, it is not possible to substitute values of other types.

Operations on booleans include:


e and e and ...	conjuction
e or e or ...	disjunction
e =\(>\) e, e not =\(>\) e	implication
not e	negation
v if e else v'	v or v' depending on e
any s, all s	disjunction / conjunction for set or list s

Integer

The integer type supports any whole number. Harmony supports decimal integers, hexadecimal integers (start with 0x), binary integers (start with 0b), and octal integers (start with 0o).

In the C-based model checker, integers are currently implemented by two's complement 60-bit words. The model checker checks for overflow on various operations.

Operations on integers include:

Operation	Description
-e	negation
abs e	absolute value
e + e + ...	sum
e - e	difference
e * e * ...	product
e / e, e // e	integer division
e % e, e mod e	integer division remainder
e e	power
~e	binary inversion
e	e
e	e
e ^ e ^ ...	binary exclusive or
e << e	binary shift left
e >> e	binary shift right
{ e..e' }	set of integers from e to e' inclusive

String

A string is a sequence of zero or more unicode characters. If it consists entirely of alphanumerical characters or underscore characters and does not start with a digit, then a string can be represented by a "." followed by the characters. For example, .example is the same as the string "example".

Native operations on strings include the following:

Operation	Description
s k	indexing
s + s + ...	concatenation
s * n	n copies of s concatenated
v [not] in s	check if v is [not] a substring in s
len s	the length of s
str e	string representation of any value e

Set

In Harmony you can create a set of any collection of Harmony values. Its syntax is { v_0, v_1, ... }. Python users: note that in Harmony the empty set is denoted as {}. (In Python, {} means the empty dictionary, which is represented as {:} in Harmony.)

The set module contains various convenient routines that operate on sets. Native operations on sets include:

Operation	Description
len s	cardinality
s -- s	set difference
s & s & ...	intersection
s \(\vert\) s \(\vert\) ...	union
s \^ s \^ ...	inclusion/exclusion (elements in odd number of sets)
choose s	select an element (Harmony will try all)
min s	minimum element
max s	maximum element
any s	`True` if any value is `True`
all s	`True` if all values are `True`

In Python, the \(<\) operator on sets represents the subset relation. However, in Harmony \(<\) is a total order. If you want to check if x is a subset of y, either use the subset method in the set module or write something like (x | y) == y (the union of x and y is y).

Harmony also supports set comprehension. In its simplest form, { f(v) for v in s } returns a set that is constructed by applying f to all elements in s (where s is a set or a list). This is known as mapping. But set comprehension is much more powerful and can include joining multiple sets (using nested for loops) and filtering (using the where keyword).

For example: { x + y for x in s for y in s where (x * y) == 4 } returns a set that is constructed by summing pairs of elements from s that, when multiplied, have the value 4.

List or Tuple

In Harmony, there is no distinction between a list or a tuple. You can denote a list by a sequence of values, each value terminated by a comma. As per usual, you can use brackets or parentheses at your discretion. For Python users, the important thing to note is that a singleton list in Harmony must contain a comma. For example [1,] is a list containing the value 1, while [1] is simply the value 1.

The list module contains various convenient routines that operate on lists or tuples. Native operations on lists or tuples include the following:

Operation	Description
t k	indexing
t + t + ...	concatenation
t * n	n copies of t concatenated
v [not] in t	check if v is [not] a value in t
len t	the length of t
min t	the minimum value in t
max t	the maximum value in t
any t	`True` if any value is `True`
all t	`True` if all values are `True`

Lists and tuples support comprehension. In its most basic form: [f(v) for v in t]. For example, to check if any element in a list t is even, you can write: any((x % 2) == 0 for x in t).

The domain of a list \(L\) of length \(n\), interpreted as a function, are the integers \(0..n-1\). It is illegal to read \(L[n]\). However, unlike Python, it is possible to write into \(L[n]\). For example, if variable x contains [1, 2], then the statement x[2] = 3 results in x having the value [1, 2, 3].

Dictionary

A dictionary maps a set of values (known as keys) to another set of values. The generic syntax of a dictionary is \(\{ k_0:v_0, k_1:v_1, ... \}\). Different from Python, the empty dictionary is written as {:} (because {} is the empty set in Harmony). If there are duplicate keys in the list, then only the one with the maximum value survives. Therefore the order of the keys in the dictionary does not matter.

Dictionaries support comprehension. The basic form is: { f(v):g(v) for v in s }.

There are various special cases of dictionaries, including lists, tuples, strings, and bags (multisets) that are individually described below.

Operations on dictionaries include the following:

Operation	Description
d k	indexing
len d	the number of keys in d
keys d	the set of keys in d
k [not] in d	check if k is [not] a value in d
min d	the minimum value in d
max d	the maximum value in d
any d	`True` if any value is `True`
all d	`True` if all values are `True`
d & d & ...	dictionary intersection
d \(\vert\) d \(\vert\) ...	dictionary union

Because in Harmony brackets are used for parsing purposes only, you can write d[k] (or d(k)) instead of d k. However, if k is a string like .id, then you might prefer the notation k.id.

Dictionary intersection and dictionary union are defined so that they work well with bags. With disjoint dictionaries, intersection and union work as expected. If there is a key in the intersection, then dictionary intersection retains the minimum value while dictionary union retains the maximum value. Unlike Python, Harmony dictionary intersection and union are commutative and associative.

Bag or Multiset

A bag is represented by a dictionary that maps each element to its multiplicity. For example: { 10:2, 12:1 } is the bag containing two copies of 10 and one copy of 12. The bag module contains various convenient routines that operate on bags. Native operations on bags include the following:

Operation	Description
v [not] in b	check if v is [not] in b
t & t & ...	bag intersection
t \(\vert\) t \(\vert\) ...	bag union

Program Counter

A program counter is an integer that can be used to index into Harmony bytecode. When you define a method, a lambda function, or a label, you are creating a constant of the program counter type.

Operations on program counters include the following:

Operation	Description
m a	invoke method with program counter m and argument a
countLabel l	return the number of threads executing at label l

You can create lambda functions similarly to Python, except that the expression has to end on the keyword end. For example: lambda(x,y): x+y end.

Address

A Harmony address is a closure consisting of a function and a list of arguments. A function can be a constant or a variable and the arguments are all Harmony values. Given an address p = ?a[b][c]..., you can use the notation !p to find its value. Harmony will first evaluate a, then apply the result to b, then apply the result to c, and so on.

As a simple example, ?5 is the address of the constant 5, and therefore !?5 evaluates to 5.

Now consider the following program:

let p = ?5:
    assert !p == 5
    !p = 5
    !p = 4

The only line in this program that fails is the last one, as you are not allowed to store 4 at the address of 5.

a can be a constant that maps Harmony values to Harmony values: dictionaries, lists, and strings. In that case, ?a[b] refers to the value of entry b in a.

The most common use of addresses is when a is a shared variable. In that case !?a evaluates to the current value of a.

Finally, a can be a program counter value (method or lambda). ?a(b) is then the closure of method a and argument b. In this case, !?a(b) evaluates a(b). For example, the following Harmony program, perhaps surprisingly, does not run into failing assertions:

counter = 0

def f():
    counter += 1
    result = counter

let p = ?f():
    if !p != 1: assert False
    if !p != 2: assert False
    if !p != 3: assert False

Internally, Harmony uses the address of a method variable and sometimes you see them on the stack during a computation. If k is a method variable, then its address is output as ?@k. However, at the Harmony language level there is no such thing as the address of a local variable. Consider the following two programs:

x = 1
let p = ?x:
    x = 2
    assert !p == 2

var x = 1
let p = ?x:
    x = 2
    assert !p == 1

In the program on the left, x is a shared variable, and ?x is the location of variable x. In the program on the right, x is a local variable. ?x evaluates x and then takes its address, so in this case ?x equals ?1.

Like C, Harmony supports the shorthand p->v for the expression (!p).v.

Context

A context value (aka continuation) captures the state of a thread. A context is itself composed over various Harmony values.

The following operations generate contexts:

`save e`	returns a Harmony value (see below)
`stop p`	saves context in `!p` and stops the thread (see below)

The save e expression, when invoked, returns a tuple (e, c) where c is the context value of the thread right after the save instruction finished. Using go c r the context can be turned into a new thread that, instead, returns r from the save e expression. See Figure A.1 for an example of how this could be used to fork a thread into two threads.

The stop p expression stores the context of the thread right after the expression in !p (i.e., p must be an address value) and terminates the thread. The thread can later be reinstantiated with go !p r, in which case the stop expression returns r. A thread can be for ever suspended using stop None or just stop().

Statements

Harmony currently supports the following statements (below, S is a list of statements and an lvalue is an expression you can use on the left-hand side of an assignment statement):

Statement	Description
e	e is an expression
lv = [lv =]... e	lv is an lvalue and e is an expression
lv [op]= e	op is one of `+`, `-`, ``, `/`, `//`, `%`, `&`, `\|`, `^`, and*, or
l: `S`	l is a label
assert b [, e]	b is a boolean. Optionally report value of expression e
await b	b is a boolean
const a = e	a is a bound variable, e is a constant expression
def m a [returns v]: `S`	m is an identifier, a a bound variable, and v a variable
del lv	delete lv
finally e	e is a boolean expression that must hold in each final state
for a[:b] in e [where c]: `S`	a and b are bound variables, e is a set, dictionary, or string
from m import ...	m identifies a module
go c e	c is a context, e is an expression
if b: `S` else: `S`	b is a boolean, `S` is a list of statements
import m, ...	m identifies a module
invariant e	e is an invariant (must always hold)
let a = e: `S`	a is a bound variable, e is an expression
pass	do nothing
print e	e is an expression
sequential v, ...	v has sequential consistency
spawn [eternal] m e [, t]	m is a method, e is an expression, t is the thread-local state
trap m e	m is a method and e is an expression
var v = e	v is a new variable, e is an expression
when b: `S`	b is a boolean, `S` a list of statements
when exists a in e: `S`	a is a bound variable, e is an expression
while b: `S`	b is a boolean, `S` a list of statements

Bound variables are read-only.
A statement can be preceded by the atomically keyword to make the statement atomic.
Multiple for statements can be combined into a single statement.
Multiple let and when statements can be combined into a single statement.

Single expression evaluation

Any expression by itself can be used as a statement. The most common form of this is a function application, for example: f(). This statement evaluates f() but ignores its result. It is equivalent to the assignment statement \(\_ = \mathtt{f}()\).

Assignment

The statement x = 3 changes the state by assigning 3 to variable x (assuming x was not already 3). x may be a local variable or a shared variable. The statement x = y = 3 first updates y, then x. The statement x[f()] = y[g()] = h() first computes the address of x[f()], then computes the address of y[g()], then evaluates h(), then assigns the resulting value to y[g()] (using its previously computed address), and finally assigns the same value to x[f()] (again using its previously computed address). The statement a,b = c assumes that c is a tuple with two values. It first evaluates the addresses of a and b and first assigns to the latter and then the former. If c is not a tuple with two values, then Harmony will report an error.

Assigning to _ (underscore) evaluates the righthand side expression but is otherwise a no-op. The left-hand side can also contain constants. For example (3, x) = (3, True) assigns True to x. However, (3, x) = (4, True) fails.

The statement \(x~+\)\(= 3\) loads x, adds 3, and then stores the results in x. In this case, it is equivalent to \(x = x + 3\). However, in general this is not so. For example, x[f()] += 3 only evaluates f() once. Unlike Python, however, x += [3,] is equivalent to x = x + [3,] in Harmony. (In Python, the following two compound statements lead to different results for y: x = y = [ ]; x += [3] and x = y = [ ]; x = x + [3].)

assert

The statement assert b evaluates b and reports an error if b is false. It should be considered a no-op---it is part of the specification, not part of the implementation of the algorithm. In particular, it specifies an invariant: whenever the program counter is at the location where the assert statement is, then b is always true.

If b is an expression, then it is evaluated atomically. Moreover, the expression is not allowed to change the state. If it does change the state, Harmony will report an error as well.

As in Python, you can specify an additional expression: assert b, e. The value of e will be reported as part of the error should b evaluate to false.

atomically

A statement can be preceded by the atomically keyword to make the statement atomic. The statement atomically: S1; S2; ... evaluates statements S1, S2, ... atomically. This means that the statement runs indivisibly---no other thread can interleave in the atomic statement. The only exception to this is if the atomic block executes a stop expression. In this case, another thread can run. When the original thread is resumed (using a go statement), it is once again atomically executing.

atomically statements are useful for specification and implementing synchronization primitives such as test-and-set. It is also useful for testing. It is not a replacement for lock/unlock, and should not generally be used for synchronization otherwise. Lock/unlock does allow other threads to run concurrently---just not in the same critical section.

await

The statement await b is equivalent to when b: pass. It is intended to improve readability of your code.

const

The expression const N = 3 introduces a new constant N with the value 3. Evaluating N does not lead to loading from a memory location. The assignment can be overridden with the -c flag: harmony -cN=4 executes the model checker with 4 assigned to N instead of 3. Harmony also supports const N, M = 3, 4, which assigns 3 to N and 4 to M. Harmony has limited support for constant folding. For example, const N = 3 + 4 assigns value 7 to constant N.

def

The statement def m a [returns v]: S1; S2: ... defines a new program counter constant m referring to a method that takes an argument a and executes the statements S1, S2, .... The argument a can be a tuple pattern similar to those used in let and for statements. Examples include (), (x,), (x, y), and (x, (y, z)). The given local variable names are assigned upon application and are read-only. Optionally, a result variable r can be declared. If not declared, there is (for backwards compatibility), a default result variable called result, initialized to None. Harmony does not support a return statement that breaks out of the code before executing the last statement.

del

The statement del x removes variable x from the state. x can be either a local or a shared variable. For example, the statement del x.age removes the .age field from dictionary x. Harmony automatically removes top-level local variables that are no longer in use from the state in order to attempt to reduce the number of states that are evaluated during model checking.

Because Harmony lists are dictionaries, deleting from lists is different from Python: del can also be used to remove elements from a list. x = [.a, .b, .c]; del x[1] results in x having value [.a, .c].

finally

The statement finally c declares that boolean expression c must hold in each final state. c is only allowed to read shared variables and is evaluated in each final state. If it evaluates to False, Harmony reports an error. Harmony also reports an error if the expression evaluates to a value other than False or True.

for ... in ... [where ...]

The statement for x in y: S1; S2; ... iterates over y and executes for each element the statements S1, S2, .... y must be a set, list, dictionary, or string. y is evaluated only once at the beginning of the evaluation of this statement. In case of a set, the result is sorted (using Harmony's global order on all values). In case of a dictionary, the statement iterates over the keys in order. This makes iterating over lists intuitive and identical to Python. For each element, the statements S1, S2, ... are executed with local variable y having the value of the element. x can be a pattern such as \((a)\) or \((a, (b, c))\). If the pattern cannot be matched, Harmony detects and error. It is allowed, but discouraged, to assign different values to x within statements S1, S2, ....

Harmony also supports the form for k:v in y: S1; S2; .... This works similar, except that k is bound to the key and v is bound to the value. If y is not a dictionary, then k ranges from 0 to len(y) - 1.

The statement also supports nesting and filtering. Nesting is of the form for x1 in y1 for x2 in y2: S1; S2; ..., which is equivalent to the statement for x1 in y1: for x2 in y2: S1; S2; .... Filtering is of the form for x in y where z: S1; S2; .... For example, for x in 1 .. 10 where (x % 2) == 0: S1; S2; ... only evaluates statements S1, S2, ... for even x, that is, 2, 4, 6, 8, and 10.

Harmony does not support break or continue statements.

from ... import

The statement from x import a, b, ... imports module x and makes its constants a, b, ... also constants in the current module. If a module is imported more than once, its code is only included the first time. The constants will typically be the names of methods (program counter constants) within the module.

You can import all constants from a module m (including program counter constants) using the statement from m import *. This, however, excludes constants whose names start with the character _: those are considered private to the module.

go

fork.hny

def fork():
    atomically:
        let (r, ctx) = save True:
            result = r
            if r:
                go ctx (False, None)

def main():
    if fork():
        print "parent"
    else:
        print "child"

spawn eternal main()

Figure A.1 (code/fork.hny): Using `save` and `go` to implement `fork()`

The statement go c e starts a thread with context c that has executed a stop or save expression. The stop or save expression returns value e. The same context can be started multiple times, allowing threads to fork. See Figure A.1 for an example.

if ... [elif ...]* [else]

Harmony supports if statements. In its most basic form, if c: S1; S2; ... evaluates c and executes statements S1, S2, ... if and only if boolean expression c evaluated to true. Harmony checks that c is either False or True---if neither is the case, Harmony reports an error. The statement if c: S1, S2, ... else: T1; T2; ... is similar, but executes statements T1, T2, ... if and only if c evaluated to False. You can think of elif \(c:\) as shorthand for else: if c:.

import

The statement import m1, m2, ... imports modules m1, m2, ... in that order. If a module is imported more than once, its code is only included the first time. The constants (including method constants) and shared variables declared in that module can subsequently be referenced by prepending "m.". For example, method f() in imported module m is invoked by calling m.f(). If you would prefer to invoke it simply as f(), then you have to import using the statement from m import f.

invariant

The statement invariant c declares that boolean expression c is an invariant. c is only allowed to read shared variables and is evaluated atomically after every state change. If it ever evaluates to False Harmony reports and error. Harmony also reports an error if the expression evaluates to a value other than False or True.

The predicate has access to two immutable variables called pre and post. post is a name for the current shared state, and thus post.x == x for any shared variable x. pre is a name for the prior shared state in a state change. For example, invariant pre.p => post.p (or equivalently invariant pre.p = p) states that p is a stable predicate: once true, it is always true. invariant pre.x <= x states that variable x grows monotonically.

Harmony (like TLA+) requires that such invariants are "invariant under stuttering", which means that for any predicate \(P\) and any reachable state \(S\) the following must hold: (pre = \(S\) = post) \(\Rightarrow P\). Less formally, \(P\) must hold in a state change that does not affect the variables that \(P\) accesses. For example, the following invariant would be problematic: invariant pre.x < x, which states that \(x\) grows strictly monotonically no matter what state changes. This is problematic because it would not hold in a state change that, say, changes \(y\) but leaves \(x\) untouched.

Invariants can be useful to specify the type of a global variable. For example, you can write invariant (type(x) == "int") and ((x % 2) == 0) to state that x is an even integer variable.

let

You can introduce new bound variables in a method using the let statement. The statement let a = b: S1; S2, ... evaluates b, assigns the result to read-only variable a, and evaluates statements S1, S2, .... let supports pattern matching, so you can write let x, (y, z) = b: S1; S2, .... This will only work if b is a tuple with two elements, the second of which also being a tuple with two elements---if not, Harmony will report an error.

let statements may be nested, such as let a1 = b1 let a2 = b2: S1; S2; .... Doing so can improve readability by reducing indentation compared to writing them as separate statements. Compare the following two examples:

let a = y:
    let b = z:
        ...

let a = y
let b = z:

pass

The pass statement does nothing.

print

The statement print e evaluates e and adds the result to the print log. The print log is used to create an "external behavior DFA" for the Harmony program.

sequential

In Harmony, shared variable Load and Store operations are atomic and have sequential consistency. However, Harmony does check for data races. A data race occurs when two or more threads simultaneously access the same shared variable, with at least one of the accesses being a Store operation outside of an atomic block. If so, Harmony will report an error. This error can be suppressed by declaring the shared variable as sequential. In particular, the statement sequential x, y, ... specifies that the algorithm assumes that the given variables have sequential consistency.

Note that few modern processors support sequentially consistent memory by default, as doing so would lead to high overhead.

spawn

The statement spawn m a starts a new thread that executes method m with argument a. m must be a program counter constant, and a is typically a tuple containing zero or more parameters to be passed to the method.

The default thread-local state of the thread, called self, is the empty dictionary by default. It can be specified by adding a parameter: spawn m a, e specifies that e should be the initial value of the thread-local state.

Harmony normally checks that all threads eventually terminate. If a thread may never terminate, you should spawn it with spawn eternal m a to suppress those checks.

trap

The statement trap m a specifies that the current thread should execute method m with argument a and some future, unspecified, time. It models a timer interrupt or any kind of asynchronous event to be handled by the thread. Such interrupts can be disabled by setting the interrupt level of the thread to True using the setintlevel operator.

var

You can introduce new local variables in a method using the var statement. The statement var a = b evaluates b and assigns the result to local variable a. var supports pattern matching, so you can write var x, (y, z) = b. This will only work if b is a tuple with two elements, the second of which also being a tuple with two elements---if not, Harmony will report an error.

when

The statement when c: S1; S2; ... executes statements S1, S2, ... after waiting until c evaluates to True. when statements are most useful when combined with the atomically keyword. If waiting is an unused local variable, then atomically when c: S1; S2; ... is equivalent to

var waiting = True
while waiting:
    atomically:
        if c:
            S1
            S2
            ...
            waiting = False

Multiple let and when statements can be combined. The expressions before the colon are re-evaluated repeated until all when conditions are satisfied.

when exists ... in ...

The statement when exists x in y: S1; S2; ... requires that y evaluates to a set value. The statement does the following three things:

it waits until y is non-empty;
it selects one element of y non-deterministically (using a choose expression);
it executes statements S1, S2, ... with the selected element bound to read-only variable x.

x may be a pattern, like in let, for, and def statements. Harmony reports an error if y evaluates to a value that is not a set.

when statements are most useful when combined with the atomically keyword. If waiting is an unused local variable, then atomically when exists x in y: S1; S2; ... is equivalent to

var waiting = True:
    while waiting:
        atomically:
            if y != {}:
                let x = choose(y):
                    S1
                    S2
                    ...
                waiting = False

The statement is particularly useful in programming network protocols when having to wait for one or more messages and executing a set of actions atomically after the desired messages have arrived.

while

The statement while c: S1; S2; ... executes statements S1, S2, ... repeatedly as long as c evaluates to True. Harmony does not support break or continue statements.

Harmony is not object-oriented

Python is object-oriented, but Harmony is not. For Python programmers, this can lead to some unexpected differences. For example, consider the following code:

x = y = [ 1, 2 ]
x[0] = 3
assert y[0] == 1

In Python, lists are objects. Thus x and y point to the same list, and the assertion would fail if executed by Python. In Harmony, lists are values. So, when x is updated in Line 2, it does not affect the value of y. The assertion succeeds. Harmony supports references to values (Chapter 7), allowing programs to implement shared objects.

Because Harmony does not have objects, it also does not have object methods. However, Harmony methods and lambdas are program counter constants. These constants can be added to dictionaries. For example, in Figure 7.1 you can add the P_enter and P_exit methods to the P_mutex dictionary like so:

{ .turn: 0, .flags: [ False, False ], .enter: P_enter, .exit: P_exit }

That would allow you to simulate object methods.

There are at least two reasons why Harmony is not object-oriented. First, object-orientation often adds layers of indirection that would make it harder to model check and also to interpret the results. Consider, for example, a lock. In Python, a lock is an object. A lock variable would contain a reference to a lock object. In Harmony, a lock variable contains the value of the lock itself. Thus, the following statement means something quite different in Python and Harmony:

x = y = Lock()

In Python, this creates two variables x and y referring to the same lock. In Harmony, the two variables will be two different locks. If you want two variables referring to the same lock in Harmony, you might write:

lock = Lock()
x = y = ?lock

or, using the alloc module,

from alloc import malloc
x = y = malloc(Lock())

The second reason for Harmony not being object-oriented is that many concurrency solutions in the literature are expressed in C or some other low-level language that does not support object-orientation, but instead use malloc and free.

Constants, Global and Local Variables

Each (non-reserved) identifier in a Harmony program refers to either a global constant, a global shared variable, a local bound variable, a local mutable variable, or a module. Constants are declared using const statements. Those constants are evaluated at compile-time.

Mutable method variables can be declared using the returns clause of a def statement or using var. Bound variables, which are immutable, can be declared in def statements (i.e., arguments), let statements, for loops, and when exists statements. Mutable variables can be declared with the var statement. Also, each method has an implicitly declared result variable, which is initialized to None. Each thread has a mutable variable called this that contains the thread-local state. Method variables are tightly scoped and cannot be shared between threads. While in theory one method can be declared within another, they cannot share local variables either. All other variables are global and must be initialized before spawned threads are start executing.

Operator Precedence

In Harmony, there is no syntactic difference between applying an argument to a function or an index to a dictionary. Both use the syntax a b c .... We call this application, and application is left-associative. So, a b c is interpreted as (a b) c: b is applied to a, and then c is applied to the result. For readability, it may help to write \(a(b)\) for function application and \(a[b]\) for indexing. In case b is a simple string, you can also write \(a.b\) for indexing.

There are three levels of precedence. Application has the highest precedence. So, !a b is interpreted as !(a b) and a b + c d is interpreted as (a b) + (c d). Unary operators have the next highest precedence, and the remaining operators have the lowest precedence. For example, \(-2 + 3\) evaluates to 1, not \(-5\).

Associative operators (\(+\), \(*\), \(|\), \(\string&\), \(\string^\), and, or) are interpreted as general \(n\)-ary operators, and you are allowed to write \(a + b + c\). However, ambiguous expressions such as \(a - b - c\) are illegal, as is any combination of operators with an arity larger than one, such as \(a + b < c\). In such cases you have to add parentheses or brackets to indicate what the intended evaluation order is, such as \((a + b) < c\).

In almost all expressions, subexpressions are evaluated left to right. So, a[b] + c first evaluates a, then b (and then applies b to a), and then c. The one exception is the expression a if c else b, where c is evaluated first. In that expression, only a or b is evaluated depending on the value of c. In the expression a and b and \(...\), evaluation is left to right but stops once one of the subexpressions evaluates to False. Similarly for or, where evaluation stops once one of the subexpressions evaluates to True. A sequence of comparison operations, such as \(a < b < c\), is evaluated left to right but stops as soon as one of the comparisons fails.

As an aside: the expression a not in b is equivalent to not (a in b). Harmony generalizes this construct for any pair of a unary (except '\(-\)') and a binary operator. In particular, a not and b is the same as not (a and b). For those familiar with logic gates, not and is the equivalent of NAND. Similarly, not =\(>\) is non-implication.

Tuples, Lists, and Pattern Matching

Harmony tuples and lists are equivalent. They can be bracketed either by '(' and ')' or by '[' and ']', but the brackets are often optional. Importantly, with a singleton list, the one element must be followed by a comma. For example, the statement x = 1,; assigns a singleton tuple (or list) to x.

Harmony does not support special slicing syntax like Python. To modify lists, use the subseq method in the list module.

Harmony allows pattern matching against nested tuples in various language constructs. The following are the same in Python and Harmony:

x, = 1,: assigns 1 to x;
x, y = 1, (2, 3): assigns 1 to x and (2, 3) to y;
x, (y, z) = 1, (2, 3): assigns 1 to x, 2 to y, and 3 to \(z\);
x, (y, z) = 1, 2: generates an runtime error because 2 cannot be matched with (y, z);
x[0], x[1] = x[1], x[0]: swaps the first two elements of list x.

As in Python, pattern matching can also be used in for statements. For example:

for key, value in [ (1, 2), (3, 4) ]: ...

Harmony (but not Python) also allows pattern matching in defining and invoking methods. For example, you can write:

def f[a, (b, c)]: ...

and then call f[1, (2, 3)]. Note that the more familiar: def g(a) defines a method g with a single argument a. Invoking g(1, 2) would assign the tuple (1, 2) to a. This is not consistent with Python syntax. For single argument methods, you may want to declare as follows: def g(\(a,\)). Calling g(1,) assigns 1 to a, while calling g(1, 2) would result in a runtime error as (1, 2) cannot be matched with (a,).

Pattern matching can also be used in const, let, and when exists statements.

### For Loops and Comprehensions While Harmony does not support general iterators such as Python does, Harmony allows iterating over sets, lists, and dictionaries. When iterating over a set, the set is always traversed in order (see Language Details for how Harmony values are ordered). When iterating over a dictionary, it is always traversed in the order of the keys.

Harmony supports nesting and filtering in for loops.

For example:
for i in { 1..10 } for j in { 1..10 } where i < j: ...
In case of dictionaries, you can access both keys and values (not supported in Python):
for k:v in .a: 1, .b: 2: ...
Harmony also supports set, list, and dictionary comprehensions. Comprehensions are similar to Python, except that filtering uses the keyword where instead of if.

Dynamic Allocation

Harmony supports various options for dynamic allocation. By way of example, consider a stack. Figure A.2 presents a test program for a stack. We present four different stack implementations to illustrate options for dynamic allocation:

Figure A.3 uses a single list to represent the stack. It is updated to perform push and pop operations;
Figure A.4 also uses a list but, instead of updating the list, it replaces the list with a new one for each operation;
Figure A.5 represents a stack as a recursively nested tuple \((v, f)\), where v is the element on top of the stack and r is a stack that is the remainder;
Figure A.6 implements a stack as a linked list with nodes allocated using the alloc module.

While the last option is the most versatile (it allows cyclic data structures), Harmony does not support garbage collection for memory allocated this way and so allocated memory that is no longer in use must be explicitly released using free.

stacktest.hny

from stack import Stack, push, pop

teststack = Stack()
push(?teststack, 1)
push(?teststack, 2)
v = pop(?teststack)
assert v == 2
push(?teststack, 3)
v = pop(?teststack)
assert v == 3
v = pop(?teststack)
assert v == 1

Figure A.2 (code/stacktest.hny): Testing a stack implementation.

stack1.hny

def Stack() returns stack:
    stack = []

def push(st, v):
    (!st)[len(!st)] = v

def pop(st) returns next:
    let n = len(!st) - 1:
        next = (!st)[n]
        del (!st)[n]

Figure A.3 (code/stack1.hny): Stack implemented using a dynamically updated list.

stack2.hny

import list

def Stack() returns stack:
    stack = []

def push(st, v):
    !st += [v,]

def pop(st) returns next:
    let n = len(!st) - 1:
        next = (!st)[n]
        !st = list.subseq(!st, 0, n)

Figure A.4 (code/stack2.hny): Stack implemented using static lists.

stack3.hny

def Stack() returns stack:
    stack = ()

def push(st, v):
    (!st) = (v, !st)

def pop(st) returns next:
    let (top, rest) = !st:
        next = top
        !st = rest

Figure A.5 (code/stack3.hny): Stack implemented using a recursive tuple data structure.

stack4.hny

from alloc import malloc, free

def Stack() returns stack:
    stack = None

def push(st, v):
    !st = malloc({ .value: v, .rest: !st })

def pop(st) returns next:
    let node = !st:
        next = node->value
        !st = node->rest
        free(node)

Figure A.6 (code/stack4.hny): Stack implemented using a linked list.

Comments

Harmony supports the same commenting conventions as Python. In particular, anything after a # character on a line is ignored. You can also enclose comments on separate lines within triple quotes. In addition, Harmony supports nested multi-line comments of the form (* comment *).

Type Checking

Harmony is dynamically typed. You can add type annotations to your program in the form of assertions and invariants. For example:

invariant (type(x) == "int") and ((x % 2) == 0)
x = choose { 0, 2, 4, 6 }

def double(n) returns result:
    assert type(n) == "int"
    result = n * 2
    assert type(result) == "int"

def main():
    x = double(x)

spawn main()

The invariant in Line~1 states that x is an even integer. The assertion in Line~5 states that the argument to function double is an integer. The assertion in Line~7 states that the return value of the function is also an integer. Harmony checks these types as it evaluates the program.