Introduction

Bismuth is a programming language designed for distributed, concurrent and mobile systems. In other words, Bismuth is designed for tasks that involve running code on multiple systems, executing code in parallel, or moving programs between systems. Despite the complex and diverse nature of these tasks, Bismuth strives to provide developers with an easy and natural mechanism for communicating these tasks while providing them with powerful correctness guarantees that can help them write better and more secure programs.

About this Guide

This document provides an introduction to Bismuth from how to get started with it to some basic documentation about it.

Types

Bismuth has both data types for describing the type of a resource in a program (e.g., a variable) as well as session types which represent the communication protocols that programs use to communicate via channels with. The former of these is often represented by an uppercase T when referring to any data type. The latter is often represented by a P when referring to any session type. These are each ellaborated in their respective sections on this page.

Data Types

Session Types

Box<T>

Boxes represent a pointer to data of a specified type, T, that is being stored on the heap.

Functions

Box<T>::init(e : T) : Box<T>

Creates a new value of type Box<T> by storing the result of evaluating the expression e : T.

Example:

Box<int> box := Box<int>::init(5); // Pointer to a value of 5 stored on the heap. 

Operators

*self : T

The dereference expression allows one to gain access to the value the box points to on the heap.

Example:

Box<int> box := ...; 

*box := 5; // Stores a value of 5 in the box
int a := *box; // Retreives the value stored in the box. 

self == Box<T> : boolean

Returns true if two boxes point to the same memory address and false otherwise.

self != Box<T> : boolean

Returns true if the two boxes point to different memory addresses.

Specifications

• Size: Pointer Size (depends on architecture) on Stack + sizeof T on the heap
• Default Location: Mixed
• Default Modifiers: Non-linear

boolean

Booleans represent a value that is either true or false.

Operators

!self : boolean

Negates the given boolean expression.

Example:

boolean a := !true;  // false 
boolean b := !false; // true 

self == boolean : boolean

Determines if two boolean expressions are equal.

Example:

boolean a := true == true;   // true 
boolean b := true == false;  // false
boolean c := false == true;  // false 
boolean d := false == false; // true

self != boolean : boolean

Determines if two boolean expressions are different.

Example:

boolean a := true != true;   // false 
boolean b := true != false;  // true 
boolean c := false != true;  // true 
boolean d := false != false; // false

self & boolean : boolean

Ands two boolean expressions with short-circuiting.

Example:

boolean a := true & true;   // true 
boolean b := false & false; // false 
boolean c := false & true;  // false 

self | boolean : boolean

Ors two boolean expressions with short-circuiting.

Example:

boolean a := true | true;   // true 
boolean b := false | false; // false 
boolena c := false | true;  // true

Specifications

• Size: 1 bit
• Default Value: false (0)
• Default Location: Stack
• Default Modifiers: Non-linear

int

Ints represents a 32-bit signed data type.

Operators

self + int : int

Performs a "No Signed Wrap (NSW)" addition of two integers. Example:

int a := 1 + 2; // 3

self - int : int

Subtracts the given integer from some other integer.

Example:

int a := 5 - 3; // 2 

self < int : boolean

Determines if the given integer is less than some other integer.

Example:

boolean a := 1 < 2; // true
boolean b := 2 < 2; // false 
boolean c := 3 < 2; // false 

self <= int : boolean

Determines if the given integer is less than or equal to some other integer.

Example:

boolean a := 1 <= 2; // true 
boolean b := 2 <= 2; // true 
boolean c := 3 <= 3; // false

self > int : boolean

Determiens if the given integer is greater than some other integer.

Example:

boolean a := 1 > 2; // false 
boolean b := 2 > 2; // false 
boolean c := 3 > 2; // true

self >= int : boolean

Determines if the given integer is greater than or equal to some other specified integer.

Example:

boolean a := 1 >= 2; // false 
boolean b := 2 >= 2; // true 
boolean c := 3 >= 2; // true

self == int : boolean

Determines if the given integer is equal to some other specified integer.

Example:

boolean a := 1 == 2; // false
boolean b := 2 == 2; // true
boolean c := 3 == 2; // false 

self != int : boolean

Determiens if the given integer is not equal to some other specified integer.

Example:

boolean a := 1 != 2; // true 
boolean b := 2 != 2; // false 
boolean c := 3 != 2; // true 

self * int : int

Multiplies the given integer with some specified integer.

Example:

int a := 3 * 2; // 6 

self / int : int

Divides the given integer by some other integer.

Example:

int a := 20 / 5; // 4 

self % int : int

Modulus of the given integer by some other specified integer.

Example:

int a := 21 % 20; // 1

Specifications

• Size: 32-bits
• Default Value: 0
• Default Location: Stack
• Default Modifiers: Non-linear

str

Strs represent constant string literals in code. Strings are defined by the text between unescaped quotation marks within the code. Strs do not yet have any methods associated with them; however, they can still be usefil (e.g., with printf statements).

Example:

str s1 := "This is a string";
str s2 := "This string contains a new line \n and a quote! \"";  

Specifications

• Size: Depends on string length
• Default Location: Data section of program file
• Default Modifiers: Non-linear

Unit

The Unit type represents a variable which can have only one possible value. For this reason, Unit rarely shows up in source code as a resource that can be assigned. Instead, Units are often used in sum types (e.g., to represent an optional).

Specifications

• Size: N/A - They do not appear in generated code.
• Default Location: N/A - They do not appear in generated code.
• Default Modifiers: Non-linear

Fixed-Length Arrays T[N]

Fixed-length arrays represent a single resource which stores N elements of type T.

Functions

self.length : int

Returns the length of the array.

Example:

int[5] a := ....; 
int a_len := a.length; // 5

Operators

self[int] : (T + Unit)

Looks up a value in the vector. If it is within bonds, the value of type T stored at the index is returned. If not, Unit is returned.

self[int] := T

Attempts to assign T to the value at the specified index.

Specifications

• Size: N * Sizeof T
• Default Location: Stack
• Default Modifiers: Non-linear

Dynamic-Length Arrays (Vectors) T[]

Ints represents a 32-bit signed data type.

Functions

self.length : u32

FIXME: WRONG TYPE

self.capacity : u32

FIXME: UNIMPLEMENTED

Operators

self[u32] : (T + Unit)

Looks up a value in the vector. If it is within bonds, the value of type T stored at the index is returned. If not, Unit is returned.

self[u32] := T : boolean

Attempts to assign T to the value at the specified index. If the index is out of bounds, the operation fails and false is returned. Otherwise, true is returned.

FIXME: NOT IMPLEMENTED; INSTEAD WE CURRENTLY PROPOGATE THE VALUE!

int + int : int

Performs a "No Signed Wrap (NSW)" addition of two integers.

int - int : int

int < int : boolean

int <= int : boolean

int > int : boolean

int >= int : boolean

int == int : boolean

int != int : boolean

int * int : int

int / int : int

int % int : int

Specifications

• Size: Sizeof Pointer + 64 bits (stack), capacity * sizeof stored data type (heap)
• Default Value: 0
• Default Location: Mixed
• Default Modifiers: Non-linear

enum

Enums (AKA. Sum Type, Tagged Union) respresent a type of data which stores a value of one of several possible types. For example, the sum type (int + boolean) would permit a resource with this type to store either an int or boolean.

The value of an enum can then be used via pattern matching.

Syntax

Enums can either be anonymous (defined in-place) or named. Anonymous enums are defined using the syntax (T_1 + ... + T_n) wherein T_1, ..., T_n are the possible types that could be stored in the sum. Note, the order of the types as specified in the enum do not matter. For example, (int + boolean) and (boolean + int) are treated as the same type.

Named enums are defined using the following syntax:

define enum <NAME> {
    T_1, 
    ..., 
    T_n
}

Unlike anonymous enums which are equivalent based on the types they can contain, named enums are seen as equal based on instance of the defined type. For example:

define enum Foo { int, boolean }

define enum Bar { int, boolean } 

Foo f := 5; 
Bar b := 5; 

if(f == b) {} // Semantic Error: Foo and Bar are different types

Foo f2 := 5; 

if (f == f2) {} // Condition will evaluate to true 

Specifications

• Size: 32-bit tag (to track type of stored value) + sizeof largest stored type
• Default Location: Stack
• Default Modifiers: Non-linear

struct

Structs (AKA. Product types) respresent a type of data which stores a value that has labeled fields of specified types.

Syntax

Structs are defined using the following syntax where T_i represents the type of the data stored by the field labeled by N_i:

define enum <NAME> {
    T_1 N_1;  
    ..., 
    T_n N_n; 
}

For example, a linked list of integers could be defined as follows:

define enum ListNode {
    int value; 
    (Unit + Box<ListNode>) next; 
}

Structs are then initialized using the syntax <NAME>::init(e_1 : T_1, ..., e_n : T_n) where e_i : T_i represents an expression e_i of type T_i whose value will be used to initialize the ith element in the struct. For example, the previous ListNode could be initialized as follows:

ListNode root := ListNode::init(1, Unit::init());
ListNode ele2 := ListNode::init(2, Unit::init()); 

Each field in the struct can then be accessed via the self.<FIELD NAME> notation. For example:

root.next := ele2; 

Specifications

• Size: Sum of the size of each element in the struct (padded as needed to have proper alignment)
• Default Location: Stack
• Default Modifiers: Non-linear

func

Functions are synchronous snippets of code that can take parameters and return a value. Currently, functions do not support capturing outside variables (they are not closures) thus, any resources they use must be provided explicitly as arguments. As functions are synchronous, arguments are passed as reference values (as opposed to programs/channels wherein data is either copied or moved).

Syntax

Functions can either be anonymous (defined in-place) or named. Anonymous funcs are defined using the syntax where T_i represents the type of the ith parameter which is named N_n, T_r is the type of data returnd by the function, and the code between the {} braces defines the body of the function:

(T_1 N_1, ... , T_n N_n) : T_r {...}

For example, an anonymous function to square a number could be defined as follows:

(int i) : int { return i * i; }

Functions can be stored as values or called in-line with their anonymous definition as shown below:

(int) -> int square := (int i) : int { return i * i; }
int result1 := (int i) : int { return i * i; }(2); // 4
int result2 := square(2); // 4

Functions can also be defined with a name to enable recursive use:

define func fib(int n) : int {
  if(n == 0 | n == 1) {
    return n;
  }

  return fib(n - 1) + fib(n - 2);
}

Specifications

• Default Location: Text/Code segment of the executable file
• Default Modifiers: Non-linear

Program

Programs are asynchronous blocks of code that can be executed and then communicated with via Channels. Because program execute asynchronously, data communicated to them via channels is copied if it is non-linear and moved if it is linear. As with functions, because programs are higher-order, they currently do not capture outside resources besides definitions. This means that any resources a program needs to execute must be communicated to it via its channel once it has been executed.

Currently programs also serve as the main entrypoint to a bismuth program. Specifically, a program named program that follows session type -int will be seen as the entrypoint.

Syntax

Programs are currently defined using the following syntax:

define <NAME> :: <CHANNEL ID> : Channel<<SESSION TYPE>> {
   // Code 
}

In this syntax, <NAME> represents the name of the program, <CHANNEL ID> is the identifier that will be bound to the channel following session type <SESSION TYPE> that the program uses to communicate back to the parent process.

For example consider the following program:

define foo :: c : Channel<-int> {
  c.send(0); 
}

In this example, we define program foo which communicates over channel c following session type -int.

Programs themselves can be treated as higher order and stored as a variable wherein they are represented by the type Program<<SESSION TYPE>> wherein <SESSION TYPE> is the session type that the program will follow when executed. For example, extending our previous example, program foo could be stored as follows:

Program<-int> prog := foo; 

Operations

exec Program<P> : Channel<dual P>

A program can be executed using the exec directive. This will return a channel that allows the process to communicate to the newly spawned program following the session type that is dual to P.

Example:

Program<-int> foo := ...; 

Channel<+int> c := exec foo; 
int i := c.recv(); 

Specifications

• Default Location: Text/Code segment of the executable file
• Default Modifiers: Non-linear

Channel<P>

Channels allow asynchronous type-safe communication between two processes. Channels are templated by a Session Type, P, to specify what operations are allowed on them at any given time.

Functions

self.send(e : T) : Unit

• Given: self : -T;P
• Action: Sends the result of evaluating expression e : T to the remote process. If e is linear, the sent value will be copied. If it is non-linear, then the value will be moved to the remote process.
• Result: self : P

self.recv() : T

• Given: self : +T;P
• Action: Receives a value of type T from the remote processs.
• Result: self : P

unfold(self) : Unit

• Given: self : ?P_1;P_2
• Action: Unfolds an interation of P_1 from ?P_1.
• Result: self : P_1;?P_1;P_2

unfold(self) : Unit

• Given: self : *?P_1;P_2
• Action: Unfolds an interation of P_1 from *?P_1 (P_1 is guarded).
• Result: self : P_1;*?P_1;P_2

more(self) : Unit

Deprecated; See unfold.

more(self) : Unit

Deprecated; See unfold.

weaken(self) : Unit

• Given: self : ?P_1T;P_2
• Action: Finishes loop ?P_1.
• Result: self : P_2

self[P_i] : Unit

• Given: self : InternalChoice<P_1, ..., P_n>
• Action: Selects protocol P_i from the internal choice to follow.
• Result: self : P_i

self[lbl_i] : Unit

• Given: self : InternalChoice<lbl_1 : P_1, ..., lbl_n : P_n>
• Action: Selects protocol P_i identified by unique label lbl_i from the internal choice to follow.
• Result: self : P_i

self.cancel() : Unit

• Since: 1.3.4
• Given: self : Cancelable<...Cancelable<P_1>;P_2>;P_3
• Action: Cancels (skips over) the innermost session type
• Result: self : Cancelable<P_2>;P_3

Channel-Specific Control Flow Operations

accept(self) {...}

• Given: self : !P_1;P_2
• Action: Allows us to repeat the loop body as many times as are requested by the remote process to fulfill !P_1. Outside of the loop, the channel thus continues as c : P_2.
• See here for details.

acceptWhile(self, e : boolean) {...}

• Given: self : !P_1;P_2 or self : *!P_1;P_2
• Action: Allows us to repeat the loop body as many times as are requested by the remote process so long as e evaluates to true. Outside of the loop, the channel thus continues as c : !P_1;P_2 or self : *!P_1;P_2 (the session is returned to its state before the acceptWhile).
• See here for details.

acceptIf(self, e : boolean) {...}

• Given: self : !P_1;P_2 or self : *!P_1;P_2
• Action: Allows us to unfold a single iteration of the of course loop so long as the remote process requests it of us and e evaluates to true. After the acceptIf, the channel thus continues as c : !P_1;P_2 or self : *!P_1;P_2 (the session is returned to its state before the acceptIf)
• Details forthcoming; however, the original Bismuth paper may be useful.

offer self (| P_i => ...)*

• Given: self : ExternalChoice<P_1, ..., P_n>
• Action: Allows us to perform a case analysis on each offered session type to allow for us to branch to a program which follows the selected session type.

Example:

// Given c : ExternalChoice<-int, +boolean;-boolean>

offer c 
  | -int => c.send(5);
  | +boolean => {
  	boolean b := c.recv(); 
  	c.send(!b);
    }

offer self (| lbl_i => ...)*

• Given: self : ExternalChoice<lbl_1 : P_1, ..., lbl_n : P_n>
• Action: Allows us to perform a case analysis on each offered session type to allow for us to branch to a program which follows the selected session type.

Example:

// Given c : ExternalChoice<sendInt: -int, recvBool: +boolean;>

offer c 
  | sendInt => c.send(5);
  | recvBool => boolean b := c.recv(); 

Specifications

• Size: TODO
• Default Location: FIXME
• Default Modifiers: Temporal, Linear

Control Flow Operations

See Also

• Channel-Specific Control Flow Operations
  • Accept
  • AcceptWhile
  • AcceptIf
  • Offer

If

If statements are used to allow code to branch depending on if their boolean condition is met. If statments can be followed by an else block to allow for an alternative to occur should the condition be false prior to the control flow merging back together.

Because of Bismuth having linear resources, type checking ensures that, regardless of how a program may branch, linear resources are used in a manner that is type safe. More details are forthcoming; however, the original Bismuth paper may be useful as this is similar to how external choices there are handled.

Syntax

If statments follows the following syntax:

if(e : boolean) // Note, parenthesis around contion are optional
{ 
  // Executed if e is true
}
else // Optional
{
  // Executed if e is false
}

See Also

• Select

Select

Select allows one to write a series of boolean conditions along with an expression. The first boolean expression to evaluate to true will have its corresponding expression evalued. This makes it similar to an if/else statement.

Syntax

select {
  e_1: e2
  ...
  e_i: e_j
}

For example:

int i := ...;
select {
  i == 1: ... // evaluated if i == 1
  i == 2: ... // evaluated if i == 2
  i == 1: ... // will never be evaluated as it is hidden by prior condition
  i < 5 : ... // evaluated if none of the prior conditions are true and and i < 5
  true: ...   // will be evaluated if none of the prior conditions are true
}

While

While loops allow a block of code to be repeated to long as the loop's boolean condition evaluates to true.

Upon entering a loop, any existing linear resources become guarded and, within loops, all non-guarded linear resources must be used. This ensures the type safe use of linear resources despite the loop's repitition. More details are forthcoming; however, the original Bismuth paper may be useful.

Syntax

While loops follows the following syntax:

while(e : boolean) { // Note, parenthesis around contion are optional
  // Loop body code
}

For example, a while loop that repeats 10 times could be written as:

int i := 0; 

while i < 10 {
  i := i + 1; 
}

For

Repeats a portion of code so long as a condition is true which is updated at the end of each iteration

Upon entering a loop, any existing linear resources become guarded and, within loops, all non-guarded linear resources must be used. This ensures the type safe use of linear resources despite the loop's repitition. More details are forthcoming; however, the original Bismuth paper may be useful.

Syntax

For loops follows the following syntax:

for((variableDeclaration | assignmentStatement); condition : boolean; statement) {
     // Loop body code
}

For example, a for loop that repeats 10 times could be written as:

for(int i := 0; i < 10; i := i + 1) {
  // Loop body code
}

This could also be written as

int i := ...; 
for(i := 0; i < 10; i := i + 1) {
  // Loop body code
}

Pattern Matching

Pattern matching can be performed on a sum type in order to access the value that it stores. Pattern matching must be exhaustive: when pattern matching on a sum, there must be a branch defined for each possible case in the sum.

Syntax

Pattern matching follows the following syntax:

match e : (T_1 + ... + T_n) 
  | T_1 <name> => ...
  | ...
  | T_n <name> => ...

For example, given the sum type (int + boolean), one could pattern match on it as follows:

(int + boolean) x := ...; 
match x 
  | int i => ... // if x stores an integer, that value can be accessed as i.  
  | boolean b => ...  // if x stores a boolean, that value can be accessed as b.  

Misc

This page outlines some of the various statements, expressions, and keywords that have not yet found their way into the other documentation pages.

<type> (<identifier 1>, ..., <identifier n> := e)*

Used to define a variable. For example:

int a := 5; 
int b, c := 6; // Both b and c equal 6 (Note: the expression for variables to be assigned to may be re-evalued for each identifier they are bound to. 
int d = 7, e = 8;

var

The keyword var can be used in place of a type name in a variable declaration. Doing so will cause the type to be inferred.

Example:

var a := 5; // a will be inferred as having type int 
var b := false; // b will be inferred as having type bool 
var c := exec Program<P>; // c will be inferred as having type Channel<dual P> 

asChannel(e : T[]) : Channel<!+T>

asChannel(e : T[N}) : Channel<!+T>

asChannel(e : T) : Channel<!+T>

• Since: 1.3.4 Given an expression e, asChannel will evaluate it and return the reuslts as a channel that can be iterated through.

Example:

int [5] a := [1, 2, 3, 4, 5];

var c2 := asChannel(a); 

# Will result in us printing "1, 2, 3, 4, 5"
accept(c2){
	int val := c2.recv();
	printf("%u ", val);
}
printf("\n");

copy(e : T) : T

Given any non-linear expression e, copy will return a deep copy of the expression. Note: parenthesis around the expression to be copied are optional.

Example:

var a := copy(5); // a will be equal to 5
var b := copy false; // b will be false

var ptr := Box<int>::init(a); 

var c := copy ptr; // c will be a deep copy of ptr

extern <Identifier> (T_1, ... T_n) : T_r

Allows one to import a function from another file/the C standard library whose name is <Identifier>, has the return type T_r, and has the arguments T_1, ..., T_n. This function is likely to be deprecated in favor of an easier system for importing resources—including other types (e.g., programs, structs, enums, etc).

import <Identifier> (:: <Identifier>)+ (as <Identifier>)?

Imports the specified definition from another file into the current file. By default, this allows one to refer to the definition via its original identifier; however, an optional identifier can be provided to rename it.

Example:

# Optional can now be used within the current scope; without
# this line, we would have to refer to it asbsl::lib::Optional::Optional
import bsl::lib::Optional::Optional; 

# Allows one to use llMap to refer to bsl::lib::Lists::map
import bsl::lib::Lists::map as llMap;

Changelog

1.3.4 (Pre-Alpha) - 2024-05-03

Features

• Added ability to use labels for describing internal and external choice alternatives
• Added dynamically sized arrays
• Added Cancelable<> session type modality
• Return statements can be omitted in functions that return Unit.
• Added Logical & Arithmetic Right Bit Shift, Left Bit Shift, Bit XOR/AND/OR
• Added imports, basic name mangling, and generics/templates
• Added u32, i64, and u64 (int and i32 are now interchangeable)
• Added ability to specify integer values in hex via 0x and binary via 0b prefixes
• Added for loops
• Added toChannel function to convert ty -> Channel<!+ty> or ty[] -> Channel<!+ty> in the case of arrays
• Added --display-mode CLI option to enable error messages to show types as they would appear in-code instead of mathematical representation
• Now displaying number of errors on compile failure

Bugs

• Fixed bug wherein T_1 -> T_2[] is ambiguous by allowing (T_1 -> T_2)[]
• Improved syntax and handling of l-values to enable expressions like improved syntax to allow *(expr). syntax,
• Fixed bug where nested control flow would incorrectly process use of linear resources
• Fixed typos in generated IR files, error messages, and compiler internals

Compiler Internals

• Reorganized compiler internals to separate CLI elements and support generics
• Refactored symbol/allocation handling by connecting them to FQNs instead of symbols
• Reorganized compilation order to conduct codegen after all of semantic analysis
• Removed CLI feature -s to supply input string instead of file location; makes more sense to re-add in future as REPL.
• Added new error type for internal/compiler errors.
• Improved efficiency of IPC by removing state to eliminate additional lookup step
• Refactored code internals to promote compile speed (of Bismuth, not the Bismuth compiler)
• Added ProtocolVisitor.cpp/.h and moved code relating to visiting protocols to there from SemanticVisitor.cpp/.h

1.3.3 (Pre-Alpha) - 2023-06-04

Features

• Added ability to nest all type defs (struct, enum) in addition to programs and functions.
• Improved syntax, particularly of externs.

1.3.2 (Pre-Alpha) - 2023-06-04

Features

• Added is_present function on ! protocols
• Added acceptIf to allow for better control over ! loops.
• Added copy(e) to allow for deep copying any non-linear e
• Added changelog to version (temporary location)

Versioning

The following outlines the versioning system for Bismuth.

Overview

Alpha

Pre-Alpha

Pre-Alpha releases of Bismuth are those which, roughly, pre-date the release of Bismuth's scource code or stem from work that Bismuth was based on. To this extent, Pre-Alpha versions are split into two groups:

• Pre-Alpha/Bismuth (versions 1.0–1.3.X) which describe the former category of releases and,
• Pre-Alpha/WPL (0.1.0.0–0.1.1.0) which identify releases in the original project Bismuth was forked from¹.

Bismuth

Given Pre-Alpha/WPL's use of versions starting with 0, Pre-Alpha/Bismuth uses versions that start with 1.

WPL

While Bismuth was created as a separate repository from WPL, given the cose ties between the initial commit in Bismuth's repository (which only started to introduce changes in transitioning from WPL to Bismuth) and WPL's v1.1.0, Bismuth's versioning scheme contains a means to refer to the initial WPL releases—though, at this point, they are largely disjoint from current development and cannot be found in the Bismuth repository.

To account for WPL using three-digit version numbers starting with 1 (i.e., 1.1.0), we refer to these as WPL/(version number) or 0.(version number) when discussing them in the context of Bismuth.