Sing Sharp

From Bauman National Library
This page was last modified on 8 June 2016, at 12:15.
Sing#
Paradigm multi-paradigm: structured, imperative, object-oriented, event-driven, functional, contract
Designed by Microsoft Research
Developer Microsoft Research
First appeared 2004
Stable release SpecSharp 2011-10-03 / October 07, 2011
Typing discipline static, strong, safe, nominative
Website Spec# website
Influenced by
C#, Eiffel

Sing# (Sing Sharp) - a type-safe, object-oriented, and garbage collected language. Sing# provides support for message-based communication. Using a type and memory safe language gurantees that memory cannot be corrupted and that all failures of the code are explicit and manifest as high-level exceptions (possibly uncaught), not random crashes or failures.

Singularity was an experimental operating system built by Microsoft Research between 2003 and 2010. It was designed as a highly-dependable OS in which the kernel, device drivers, and applications were all written in managed code.

The lowest-level x86 interrupt dispatch code is written in assembly language and C. Once this code has done its job, it invokes the kernel, whose runtime and garbage collector are written in Sing# (an extended version of Spec#, itself an extension of C#) and runs in unprotected mode. The hardware abstraction layer is written in C++ and runs in protected mode. There is also some C code to handle debugging. The computer's BIOS is invoked during the 16-bit real mode bootstrap stage; once in 32-bit mode, Singularity never invokes the BIOS again, but invokes device drivers written in Sing#.

Features

Channel Contracts

Channel contracts are central to Singularity’s isolation architecture and are directly supported in Sing#. Here’s a contract describing a simple interaction on a channel.

contract C1 {
   in message Request(int x) requires x>0;
   out message Reply(int y);
   out message Error();

   state Start: Request?
                -> (Reply! or Error!)
                -> Start;
}

Contract C1 declares three messages: Request, Reply, and Error. Each message specifies the types of arguments contained in the message. For example, Request and Reply both contain a single integer value, whereas Error does not carry any values. Additionally, each message may specify Spec# requires clauses restricting the arguments further.

Messages can also be tagged with a direction. The contract is always written from the exporter point of view. Thus, in the example, Request is a message that can be sent by the importer to the exporter, whereas Reply and Error are sent from the exporter to the importer. Without a qualifier, messages can travel in both directions.

Endpoints

Channels in Singularity manifest as a pair of endpoints representing the importing and exporting sides of the channel. Each endpoint has a type that specifies which contract the channel adheres to. Endpoint types are implicitly declared within each contract. A contract C1 is represented as a class, and the endpoint types are nested types within that class as follows:

  • C1.Imp — Type of import endpoints of channels with contract C1.
  • C1.Exp — Type of export endpoints of channels with contract C1.

Send/receive Methods

Each contract class contains methods for sending and receiving the messages declared in the contract. The example provides the following methods:

C1.Imp {
   void SendRequest(int x);
   void RecvReply(out int y) ;
   void RecvError();
}

C1.Exp {
   void RecvRequest(out int x)
   void SendReply(int y);
   void SendError();
}

The semantics of the Send methods are that they send the message asynchronously. The receive methods block until the given message arrives. If a different message arrives first, an error occurs. Such errors should never occur if the program passes the contract verification check. Unless a receiver knows exactly which message it requires next, these methods are not appropriate. Instead, Sing# provides a switch receive statement.

Switch-Receive Statement

Consider the following code, which waits for either the Reply or Error message on an imported endpoint of type C1.Imp.

void M( C1.Imp a) {
   switch receive {
      case a.Reply(x):
         Console.WriteLine(“Reply {0}”, x);
         break;
      case a.Error():
         Console.WriteLine(“Error”);
         break;
   }
}

The switch receive statement operates in two steps:

  1. Block for a particular set of messages to arrive on a set of endpoints;
  2. Receive one of the set of messages and bind its arguments into local variables.

In the example above, the switch receive has two patterns, either receive Reply on endpoint a, or Error on the same endpoint. In the first case, the integer argument of the Reply message is automatically bound to the local variable x.

The switch receive construct is however more general, as patterns can involve multiple endpoints. The following example has two endpoints a and b that can receive Reply or Error messages:

void M (C1.Imp a, C1.Imp b) {
   switch receive {
      case a.Reply(x) && b.Reply(y):
         Console.WriteLine(“Both replies {0} and {1}”, x, y);
         break;

      case a.Error():
         Console.WriteLine(“Error reply on a”);
         break;

      case b.Error():
         Console.WriteLine(“Error reply on b”);
         break;

      case a.ChannelClosed():
         Console.WriteLine(“Channel a is closed”); 
         break;
   }
}

Ownership

In order to guarantee memory isolation of endpoints and other data transferred on channels, all blocks in the Exchange Heap are resources that need to be tracked at compile time. In particular, the static checks enforce that access to these resources occur only at program points where the resource is owned and that methods do not leak ownership of the resources. Tracked resources have a strict ownership model. Each resource is owned by at most one thread (or by a data structure within a thread) at any point in time. For example, if an endpoint is sent in a 18 message from thread T1 to thread T2, then ownership of the endpoint changes: from T1 to the message and then to T2, upon messages receipt.

TRefs

A TRef is a storage cell of type TRef<T> holding a tracked data structure of type T. TRef has the following signature:

class TRef<T> where T:ITracked {
   public TRef([Claims] T i_obj);
   public T Acquire();
   public void Release([Claims] T newObj);
}

When creating a TRef<T>, the constructor requires an object of type T as an argument. The caller must have ownership of the object at the construction site. After the construction, ownership has been passed to the newly allocated TRef. The Acquire method is used to obtain the contents of a TRef. If the TRef is full, it returns its contents and transfers ownership to the caller of Acquire. Afterwards, the TRef is said to be empty. Release transfers ownership of a T object from the caller to the TRef. Afterwards, the TRef is full. TRefs are thread-safe and Acquire operations block until the TRef is full.

The Exchange Heap

Since ownership of blocks of memory is transferred from one thread or process to another on message exchanges, Singularity needs a way to allocate and track blocks that can be exchanged in this fashion. The channel system requires that message arguments be either scalars or blocks in the Exchange Heap. There are two kinds of blocks in the Exchange Heap: individual blocks or vectors. Their types are written, respectively, as follows:

using Microsoft.Singularity.Channels;
R* in ExHeap pr;
R[] in ExHeap pv;

Compile-Time Reflection

Generators are written in Sing# as transforms. A transform contains a pattern matching program structure and a code template to build new code elements. Combining these two enables a transform to be analyzed and checked independent of the code to which it will be applied. For example, errors, such as generating a call on a non-existent method or calling with the wrong type of object, can be detected in a transform. In this respect, CTR is similar to multi-stage languages. Note that a CTR transform may be part of the trusted computing base, and so it can emit trusted code into an otherwise untrusted process.

transform DriverTransform
      where $IoRangeType: IoRange {

   class $DriverCategory: DriverCategoryDeclaration {
      [$IoRangeAttribute(*)]
      $IoRangeType $$ioranges;
 
      public readonly static $DriverCategory Values;
 
      generate static $DriverCategory() {
         Values = new $DriverCategory();
      }

      implement private $DriverCategory() {
         IoConfig config = IoConfig.GetConfig();
         Tracing.Log(Tracing.Debug, "Config: {0}", config.ToPrint());

         forall ($cindex = 0; $f in $$ioranges; $cindex++) {
            $f = ($f.$IoRangeType) config.DynamicRanges[$cindex];
         }
      }
   }
}

Sources