Online / 5 & 6 February 2022

visit

Designing a new Language for Safety: Fuzion

A minimal language for safety-critical systems


Fuzion is a modern general purpose programming language that unifies concepts found in structured, functional and object-oriented programming languages into the concept of a Fuzion feature. It combines a powerful syntax and safety features based on the design-by-contract principle with a simple intermediate representation that enables powerful optimizing compilers and static analysis tools to verify correctness aspects.

This talk will focus on Fuzion's aspects related to safety-critical software development. A fundamental idea of Fuzion is to provide a simple language at a high level of abstraction and move implementation decisions from the developer to the compiler. To enable this, the language defines a simple but powerful intermediate representation for static analysis tools to operate on.

Furthermore, pre- and post-conditions for design-by-contract are provided in a way that enables different levels of verification: static analysis as well as dynamic checks at different levels from safety to debugging.

Fuzion does not support exceptions, a run-time error has to be part of the result of a call and must be checked explicitly. Fuzion does not support dynamic loading of code. Numeric operations such as 'infix +' check for overflow.

Fuzion applications consist of a set of library modules and a main modules. Modules are verified for correctness individually as well as whole applications. This is possible since dynamic loading of code is not supported.

Introduction

Fuzion is a modern general purpose programming language that unifies concepts found in structured, functional and object-oriented programming languages into the concept of a Fuzion feature. It combines a powerful syntax and safety features based on the design-by-contract principle with a simple intermediate representation that enables powerful optimizing compilers and static analysis tools to verify correctness aspects.

Fuzion was influenced by many other languages including Java, Python, Eiffel, Rust, Go, Lua, Kotlin, C#, F#, Nim, Julia, Clojure, C/C++, and many more. The goal of Fuzion is to define a language that has the expressive power present in these languages and allow high-performance implementations and powerful analysis tools. Furthermore, Fuzion addresses requirements for safety-critical applications by adding support for contracts that enable formal specification and enable detailed control over run-time checks.

Many current programming language are getting more and more overloaded with new concepts and syntax to solve particular development or performance issues. Languages like Java/C# provide classes, interfaces, methods, packages, anonymous inner classes, local variables, fields, closures, etc. And these languages are currently further extended by the introductions of records/structs, value types, etc. The possibility of nesting these different concepts results in complexity for the developer and the tools (compilers, VMs) that process and execute the code.

For example, the possibility to access a local variable as part of the closure of a lambda expression may result in the compiler allocating heap space to hold the contents of that local variable. Hence, the developer has lost control over the allocation decisions made by the compiler.

In Fuzion, the concepts of classes, interfaces, methods, packages, fields and local variables are unified in the concept of a Fuzion feature. The decision where to allocate the memory associated with a feature (on the heap, the stack or in a register) is left to the compiler just as well as the decision if dynamic type information is needed. The developer is left with the single concept of a feature, the language implementation takes care of all the rest.

Fuzion Feature Declarations

A Fuzion feature has a name, similar to the name of a class or a function. The main operation that can be performed on a feature is a feature call. The constituents of a feature declaration are as follows:

Formal Arguments

Features may have a list of formal arguments, which are themselves features implemented as fields. On a call to a feature with formal arguments, actual arguments have to be provided to the call, unless the list of formal arguments is empty.

Feature Result

The result of a feature call is an instance of the feature. Alternatively, a feature may declare a different result type, then it must return a value of that type on a call.

Closures

Features are nested, i.e., every feature is declared within the context of an outer feature. The only exception is the universe, which is the outermost feature in Fuzion. A feature can access features declared in its outer feature or, recursively, any outer feature of these outer features. This means, a feature declaration also defines a closure of the feature and its context.

When calling a feature f1 declared as an inner feature of f2, the call must include a target value which is the result of a call to f2, e.g., f2.f1.

Generics

Features may have generic type parameters. E.g. a feature declaration may leave the actual type used within that feature open and to be defined by the user of the feature.

The list of generic type parameters may be open, i.e., the number of actual generic type parameters is not fixed at feature declaration. This turns out to be useful in the declaration of choice types and functions as explained below.

Inheritance

Fuzion features can inherit from one or several other features. When inheriting from an existing features, all inner features of the parent automatically become inner features of the heir feature. It is possible to redefine inherited features. In particular, when inheriting from a feature with abstract inner features, one can implement the inherited abstract features.

A redefinition of an inherited feature may implement an inherited feature as a routine or as a field. An inherited feature that is implemented as a field, however, cannot be redefined as something else since fields might be mutable.

Inheritance may result in conflicts. An example would be two features with the same name that are inherited from two different parents. In this case, the heir must resolve the conflict either by redefining the inherited features and providing a new implementation or by renaming the inherited features resulting in two inner features in the heir feature.

Inheritance and redefinition in Fuzion does not require dynamic binding. By default, the types defined by features are value types and no run-time overhead for dynamic binding is imposed by inheritance.

A Contract

A feature may declare a contract that specifies what the features does and under which conditions the feature may be called.

An implementation

Features must have one of the following implementations

  • a routine is a feature implementation with code that is executed on a call

  • a field is a memory slot that stores a value and whose contents are returned on a call

  • an abstract feature has no implementation and cannot be called directly, but can be implemented by heir features

  • an intrinsic feature is a low-level feature implemented by the compiler or run-time system, e.g., the infix + operator to add two 32-bit integer values may be an intrinsic operation.

A feature implemented as a routine can contain inner feature declarations.

Feature examples

Here is an example that declares a feature point that functions similar to a struct or record in other languages:

point(x, y i32) is # empty
p1 := point 3 4
say "p1.x is {p1.x}"    # will print "p1.x is 3"
say "p1.y is {p1.y}"    # will print "p1.y is 4"

The next example shows a feature base that provides an inner feature plus that adds its argument to the value passed to the enclosing base:

base(v i32) is
  plus(w i32) => v + w

b1 := base 30
b2 := base 100
say (b1.plus 23)    # will print "53"
say (b2.plus 23)    # will print "123"

Design-by-Contract

Fuzion features can be equipped with pre- and post-conditions to formally document the requirements that must be met when a feature is called and the guarantees given by a feature. An example is a feature that implements a square root function for 32-bit integers:

sqrt(a i32) i32

pre
  safety: a >= 0
post
  debug: result * result <= a,
  debug: (result + 1) > a / (result + 1),
  debug: result >= 0

is

if a == 0
  0
else
  for
    last := 0, r
    r    := 1, (last +^ a / last) / 2         # +^ performs saturating addition
  until r == last

In this case, the function defines the pre-condition that its argument 'a' is non-negative. A call of this function with a negative value will result in a run-time error. On the other hand, its post-conditions make a clear statement about the result: The result will be the largest value that, when squared, is less than or equal to 'a'.

Checking Pre- and Post-conditions

Pre- and post-conditions can be classified for different purposes. Default qualifiers provided in the standard library are

safety

This qualifier protects pre-conditions that are required for the safety of an operation.

An example is the index check pre-condition of the intrinsic operation to access an element of an array: Not performing the index check would allow arbitrary memory accesses and break the application's safety.

This qualifier should therefore never be disabled unless you are running code in an environment where performance is essential and safety is irrelevant.

debug, debug(n)

This qualifier is generally for debugging, it is set iff debugging is enabled or enabled at the given level, respectively..

pedantic

This qualifier is for conditions that a pedantic purist would require, that otherwise a more relaxed hacker would prefer to do without.

analysis

Qualifier for conditions that are generally not reasonable as run-time checks, either because they are prohibitively expensive or even not at all computable in this finite universe. These conditions may, however, be useful for formal analysis tools that do not execute the code but perform techniques such as abstract interpretation or formal deduction to reason about the it.

Additional user defined qualifiers may be added, any expression resulting in a 'bool' can be used.

Run-time checks for pre- and post-conditions can be enabled or disabled for each of these qualifiers (except for 'analysis', which is always disabled). This gives a fine-grain control over the kind of checks that are desired at run-time. Usually, one would always want to keep safety checks enabled in a system that processes data provided from the outside to avoid vulnerabilities such as buffer overflows. However, in a closed system like a rocket controller, it might make sense to disable checks since a run-time error would mean definite loss of the mission, while an unexpected intermediate value may still result in a useful final result of a calculation.

Explicit results instead of Exceptions

Instead of exceptions that provide an alternative path for a function to return, Fuzion requires all functions to return a result. To indicate failure, the generic result type 'outcome' is provided.

outcome is a choice type that represents the result of a routine that may either produce something useful or fail producing an error condition.

Here is a small example of using an outcome result

getData (u User, t Type) outcome<data> is

if u.allowedToAcces T
  (readFile t.fileName)?
else
  error "user $u not allowed to access $t"

readFile (n string) outcome<data> is

if dataExists n
  readData n
else
  error "data $t not available"

A user of this code when would have to explicitly unwrap the read data as follows

o := getData user type match o

d data  => say "success: $d"
e error => say "*** error $e"

Fuzion Modules

Modules in Fuzion are collections of Fuzion features that form a library to be used by other modules. Modules may define a main entry point, such that they can be used to build applications.

The Fuzion front end performs static code analysis at the module level. This means that any features exported by a module are save to be used in different contexts by other modules. This includes static checking of the following aspects:

Field Initialization

In Fuzion, the front end ensures that all fields are assigned an initial value. There is no default initial value for uninitialized fields and there is no means to access an uninitialized fields, as there is, e.g., for final fields in Java.

Instead, it is checked that whenever an instance containing a field becomes accessible outside of the feature declaring that field, the call chain is analyzed to ensure it may not contain any accesses to the field. In particular, if an instance may become visible outside of the module, no uninitialized field may be accessible by any exported features of that module.

Function Purity

The result of any feature visible to the outside must be independent of state modifiable by other exported features and must not itself modify state that may affect the result of other exported features. This purity will allow optimizations such as memoization or lazy evaluation common in functional languages.

Nevertheless, a pure function may use mutable fields, e.g., to store intermediate results during its calculations. If the mutable field's life span is limited to the call of the exported feature and the field is not accessed by any other exported feature, mutation does not make a function impure.

Race Freedom

Closely related to function purity is race freedom: Any exported feature is checked to be safe to be called in a threaded environment without causing data races. There are no explicit locks in Fuzion, so there is no danger of deadlocks due to nested locking.

Immutability

Fuzion encourages the use of immutable data by simple syntax for the declaration of immutable fields. Also, the use of tail calls for loops automatically converts iterator variables used in that loop into immutable variables with a life span of a single loop iteration.

Since immutability is essential to ensure correctness of parallel execution within threads that do not rely on locks or similar synchronization mechanisms, Fuzion's analyzer will verify that data shared between threads is immutable.

The standard library has been designed to provide immutable data types. Nevertheless, there are mutable types such as 'marray', which provides a mutable array. These, however, should be used for local calculations only, escape analysis will ensure that no accesses to mutable types occur from outside the code manipulating the state.

Memory Management

Fuzion to a large extend relies on static analysis to reduce memory management overhead. Instances are by default value instances that do not require heap allocation. Furthermore, immutability in many cases avoids the need to keep a shared copy on the heap. For dynamic calls, heap allocation and dynamic binding overhead is avoided by specialization of calls.

Only for those instances for which all of these optimizations would fail, in particular instances shared between threads or long-lived instances with mutable fields, heap allocation will be required. Memory allocated on the heap will be reclaimed by a real-time garbage collector.

Fuzion Thread Safety

Static analysis at module and application level ensure that mutable data is not shared between threads in Fuzion. However, there must be means for threads to communicate, e.g., for the result of a thread to become available to other threads. How this will be done in Fuzion is still open, thread safe libraries such as thread-safe queues between might be provided here.

Conclusion and Next Steps

I hope Fuzion shows some interesting ideas how to approach the development of safety-critical software.

The Fuzion language definition and implementation are far from stable, but are getting closer to become useful. Currently, two execution options for Fuzion are available: An interpreter implemented in Java and a back-end that compiles to C code. A tool to interface Java code is available for the interpreter.

Main points that are missing right now are

  • a powerful standard library
  • additional library modules for all sorts of application needs
  • low-level foreign language interface for C
  • actual implementations of static analyzers and optimizers
  • highly optimizing back-ends
  • garbage collection for the C back-end
  • documentation, tutorials
  • enthusiastic contributors and users!

Please feel free to contact me in case you want to use Fuzion or want to help making it a success!

Speakers

Photo of Fridtjof Siebert Fridtjof Siebert

Attachments

Links