Sing Sharp

Материал из Национальной библиотеки им. Н. Э. Баумана
Последнее изменение этой страницы: 15:15, 8 июня 2016.
Sing#
Парадигма мультипарадигменный: структурный, императивный, объектно-ориентированный, событийно-ориентированный, функциональный, контрактный
Спроектировано Microsoft Research
Разработчики Microsoft Research
Печать дисциплины статическая, строгая, типобезопасная, номинативная
Лицензия Microsoft Research License
Портал: Spec# website

Sing# (Sing Sharp, произносится sɪŋ ʃɑːp ) — язык программирования с поддержкой параллелизма, является расширением языка программирования Spec#, который, в свою очередь, является расширением языка C#. Microsoft Research разработала Spec#, и позднее расширила его, превратив в Sing#, для разработки операционной системы Singularity. Sing# расширяет возможности Spec# за счет поддержки каналов и конструкций низкоуровневого языка программирования, необходимых для реализации системного ПО. Язык Sing# типобезопасный. Семантика примитивов обмена данными (message-passing primitives) в языке Sing# фиксирована и описывается формальными соглашениями.

Обзор

Sing#, типобезопасный, объектно-ориентированный язык со сборщиком мусора. Sing# обеспечивает поддержку для связи на основе сообщений. Использование языка, который обеспечивает безопасную работу с памятью, позволяет избегать многих ошибок при работе с ней. Ошибки проявляются лишь явно и в виде исключения на высоком уровне (возможно, не перехваченные), а не случайные сбои или ошибки.

Язык Sing# изначально создавался для разработки операционной системы Singularity. Singularity — начатый в 2003 году проект исследовательского подразделения корпорации Microsoft по созданию высоконадёжной операционной системы, в которой микро ядро, драйверы устройств и приложения написаны на управляемом коде. Низкоуровневый код обработки прерываний x86 написан на языке ассемблера и C. Библиотеки времени исполнения (англ. runtime) и сборщик мусора написаны на Sing# с использованием небезопасного режима (англ. unsafe mode). Также присутствует код на C, использующийся в целях отладки. BIOS компьютера вызывается только на этапе загрузки в 16-разрядном реальном режиме работы процессора. После перехода в 32-разрядный режим, BIOS больше никогда не вызывается, вместо него используются драйверы, написанные на Sing#.

Возможности

Канальные контракты

Канальные контракты занимают центральное место в изоляционной архитектуре Singularity и напрямую поддерживаются в Sing#. Вот контракт, описывающий простое взаимодействие по каналу.

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;
}

Контракт С1 заявляет три сообщения: Request, Reply и Error. Каждое сообщение определяет типы аргументов, содержащихся в сообщении. Например Request и Reply содержат одно целое значение, в то время как Error не несет каких-либо значений. Кроме того, каждое сообщение может использовать Spec#, чтобы ограничить количество аргументов.

Сообщения могут быть помечены направлением. Контракт всегда пишется со стороны экспортера. Таким образом, в примере, Request - сообщение, которое может быть отправлено импортером экспортеру, тогда как Reply и Error отправляются от экспортера к импортеру. Без классификатора, сообщения могут путешествовать в обоих направлениях.

Конечные точки

Каналы в Singularity представляются в виде пары конечных точек, представляющих импортеров и экспортеров каждой стороны канала. Каждая конечная точка имеет тип, который определяет, какому контракту принадлежит канал. Типы конечных точек неявно объявляются внутри каждого контракта. Контракт С1 представлена как класс, и оконечные типы вложенных типов внутри этого класса следующим образом:

  • C1.Imp - Тип импортируемых конечных точек каналов с контракта С1.
  • C1.Exp - Тип экспортируемых конечных точек каналов с контракта С1.

Методы отправки и получения

Каждый класс контракта содержит методы отправки и получения сообщений, объявленных в контракте. Пример:

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();
}

Семантика методов отправки проявляется а том, чтобы передать сообщение асинхронно. Принимаемые методы блокируются, пока не прибудет заданное сообщение. Если другое сообщение прибывает первым, возникает ошибка. Такие ошибки не должны возникать, если программа проходит проверку подлинности контракта. Если приемник не знает точно, какое сообщение он должен получить следующим, ни один из методов не подойдёт. Вместо этого, Sing# позволяет коммутатору получить объявление.

Изменение получаемого метода

Рассмотрим следующий код, который ждет Reply или Error на 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;
   }
}

Изменение получаемого метода происходит в два этапа:

  1. Блокировка определённого набора сообщения до получения множества конечных точек;
  2. Получить одно из множества сообщений и связать его аргументы с локальными переменными.

В приведенном выше примере, коммутатор либо получает два шаблона, либо получает Reply на конечной линии, либо же Error на конечной точке. В первом случае, целый аргумент из Reply сообщения автоматически привязывается к локальной переменной х.

Коммутатор в основном получает более общую конструкцию, в то время как шаблоны могут включать в себя несколько конечных точек. В следующем примере две конечные точки a и b, которые могут получить Reply или Error:

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;
   }
}

Принадлежность

Для того, чтобы гарантировать изоляцию памяти конечных точек и других данных, передаваемых по каналам, все блоки в Exchange и Heap - являются ресурсами, которые нужно отслеживать при компиляции. В частности, статические проверки соблюдения правил того, что доступ к этим ресурсам будет происходить только в тех местах программы, которым принадлежит ресурс и что методы не лишаются своих ресурсов. Наблюдаемые ресурсы имеют строгую модель собственности. Каждому ресурсу принадлежит не более одного потока (или по структуре данных внутри потока) в любой момент времени. Например, если конечная точка передает 18 сообщений от потока T1 - потоку T2, то право собственности изменяется следующим образом: T1 - на сообщение, а затем Т2 - на получаемое сообщение.

TRefs

TRef - ячейка хранения типа TRef<T>, которая содержит отслеживаемую структуру данных типа T. TRef имеет следующую подпись:

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

При создании TRef<T>, конструктор требует объект типа T в качестве аргумента. Вызывающий должен иметь право собственности на объект на стороне конструкции. После создания, право собственности будет передано во вновь выделенный TRef. Метод Acquire используется для получения содержимого TRef. Если TRef полон, она возвращает его содержимое и передает право собственности методу Acquire. После этого TRef считается пустым. Release передает право собственности на объект T от вызывающей стороны к TRef. После этого TRef полна.

Куча обмена

С того момента, как управление блоками памяти передается от одного потока или процесса к другому на биржах сообщений, Singularity нужен способ выделить и проследить блоки, которые могут быть обменены таким образом. Система каналов требует, чтобы аргументы сообщений были либо скаляры, либо блоками в куче обмена. Есть два вида блоков в куче обмена: индивидуальные блоки или векторы. Их типы записываются соответственно, следующим образом:

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

Отражение времени компиляции

Генераторы пишутся на Sing# как преобразования. Преобразование содержит программную структуру сопоставления с образцом и шаблон кода для создания новых элементов кода. Сочетание этих двух элементов дает преобразование для анализа и проверку зависимости от кода, к которому он будет применяться. Например, ошибки, такие как генерирование вызовов на несуществующие методы или вызов с неправильным типом объекта, могут быть обнаружены в преобразованиях. В этом отношении CTR похожа на многоструктурные языки. Обратите внимание, что CTR преобразование может быть частью доверенной вычислительной базы, и поэтому она может выполнять доверенный код, в противном случае - ненадежный процесс.

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];
         }
      }
   }
}

Литература

Ссылки

  1. https://ru.wikipedia.org/wiki/Sing_Sharp