Тип сеанса
Типовые системы
Общие понятия
Основные категории
Второстепенные категории

В теории типов типы сеансов используются для обеспечения корректности в параллельных программах. Они гарантируют, что сообщения, отправленные и полученные между параллельными программами, находятся в ожидаемом порядке и имеют ожидаемый тип . [1] [2] Системы типов сеансов были адаптированы как для систем каналов , так и для систем акторов . [3]

Типы сеансов используются для обеспечения желаемых свойств в параллельных и распределенных системах, т. е. отсутствия ошибок связи или взаимоблокировок, а также соответствия протоколам. [4]

Двоичные и многосторонние типы сеансов

Взаимодействие между двумя процессами можно проверить с помощью бинарных типов сеансов, в то время как взаимодействие между более чем двумя процессами можно проверить с помощью многосторонних типов сеансов. [5] В многосторонних типах сеансов взаимодействие между всеми участниками описывается с помощью глобального типа , который затем проецируется в локальные типы , которые описывают коммуникацию с локального представления каждого участника. Важно, что глобальный тип кодирует информацию о последовательности коммуникации, которая была бы потеряна, если бы мы использовали бинарные типы сеансов для кодирования той же коммуникации. [6]

Формальное определение типов бинарных сеансов

Типы двоичных сеансов можно описать с помощью операций отправки ( ), операций получения ( ), ветвлений ( ), выборок ( ), рекурсии ( ) и завершения ( ). [2] ! {\displaystyle !} ? {\стиль_дисплея ?} & {\displaystyle \&} ⊕ {\displaystyle \oplus} г е с {\displaystyle запись} е н г {\displaystyle конец}

Например, представляет собой тип сеанса , который сначала отправляет логическое значение ( ), затем получает целое число ( ) и, наконец, завершается ( ). С = ! б о о л . ? я н т . е н г {\displaystyle S=\;!bool.?int.end} С {\displaystyle S} ! б о о л {\displaystyle !bool} ? я н т {\displaystyle ?целое} е н г {\displaystyle конец}

Реализации

Типы сеансов были адаптированы для нескольких существующих языков программирования, включая:

  • lchannels ( Scala ) [7]
  • Эффи (Scala) [7]
  • STMonitor (Scala) [8]
  • Ансамбли [9]
  • Типы сессий ( Rust ) [10]
  • сеш (Ржавчина) [11]
  • Актеры сеанса ( Python ) [12]
  • Контролируемый сеанс Erlang ( Erlang ) [13]
  • FuSe ( OCaml ) [14]
  • сеанс-ocaml (OCaml) [15] [16]
  • Приоритетный Sesh ( Haskell ) [17]
  • Проверка состояния типов Java ( Java ) [18] [19] [20]
  • Сессии Swift ( Swift ) [21]

Ссылки

  1. ^ Хюттель, Ганс; Ланезе, Иван; Васконселос, Васко Т.; Кайрес, Луис; Карбоне, Марко; Дениелу, Пьер-Мало; Мостроус, Димитрис; Падовани, Лука; Равара, Антониу; Туосто, Эмилио; Виейра, Уго Торрес; Заваттаро, Джанлуиджи (5 апреля 2016 г.). «Основы типов сеансов и поведенческих контрактов». Обзоры вычислительной техники ACM . 49 (1): 3:1–3:36. дои : 10.1145/2873052. hdl : 2381/38761 . ISSN  0360-0300. S2CID  3580137.
  2. ^ ab Ancona, Davide (2016). Поведенческие типы в языках программирования. Ганновер, Массачусетс: Now Publishers. ISBN 978-1-68083-135-1. OCLC  1053840486.
  3. ^ Фаулер, Саймон; Линдли, Сэм; Уодлер, Филип (10 мая 2017 г.). «Смешивание метафор: актеры как каналы и каналы как актеры (расширенная версия)». arXiv : 1611.06276 [cs.PL].
  4. ^ Скалас, Альцесте; Ёсида, Нобуко (июнь 2018 г.). «Типы многосторонних сеансов, за пределами дуальности». Журнал логических и алгебраических методов в программировании . 97 : 55–84 . doi : 10.1016/j.jlamp.2018.01.001 . hdl : 10044/1/56777 . S2CID  48360420.
  5. ^ Хонда, Кохей; Ёсида, Нобуко; Карбоне, Марко (2008). «Типы многосторонних асинхронных сеансов». Труды 35-го ежегодного симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования. стр.  273–284 . doi :10.1145/1328438.1328472. hdl :10044/1/26368. ISBN 9781595936899. S2CID  53038488.
  6. ^ Ёсида, Нобуко; Гери, Лоренцо (2019). Очень деликатное введение в типы многосторонних сеансов . ICDCIT 2020. doi :10.1007/978-3-030-36987-3_5.
  7. ^ ab "Программирование сеансов в Scala". alcestes.github.io . Получено 2 ноября 2021 г. .
  8. ^ "STMonitor". chrisbartoloburlo.github.io . Получено 2 ноября 2021 г. .
  9. ^ Харви, Пол; Фаулер, Саймон; Дардха, Орнела; Гей, Саймон Дж. (2021). «Типы многосторонних сеансов для безопасной адаптации времени выполнения в языке акторов». 35-я Европейская конференция по объектно-ориентированному программированию (ECOOP 2021) . 194 : 10:1–10:30. doi : 10.4230/LIPIcs.ECOOP.2021.10 . S2CID  234681015.
  10. ^ Йесперсен, Томас Брахт Лауманн; Мунксгаард, Филип; Ларсен, Кен Фриис (30 августа 2015 г.). «Типы сессий для Rust». Материалы 11-го семинара ACM SIGPLAN по общему программированию . WGP 2015. Ассоциация вычислительной техники. стр.  13–22 . doi : 10.1145/2808098.2808100. ISBN 9781450338103. S2CID  18320631.
  11. ^ Кокке, Вэнь (12 сентября 2019 г.). «Rusty Variation: Deadlock-free Sessions with Failure in Rust». Electronic Proceedings in Theoretical Computer Science . 304 : 48– 60. arXiv : 1909.05970 . doi : 10.4204/EPTCS.304.4. ISSN  2075-2180. S2CID  198166990.
  12. ^ Ёсида, Нобуко; Нейкова, Румяна (29 марта 2017 г.). «Акторы многопартийного сеанса». Логические методы в информатике . 13 (1). doi :10.23638/LMCS-13(1:17)2017. S2CID  65240382.
  13. ^ Фаулер, Саймон (10 августа 2016 г.). «Реализация многопартийных сеансовых актеров на языке Erlang». Электронные труды по теоретической информатике . 223 : 36–50 . arXiv : 1608.03321 . doi :10.4204/EPTCS.223.3. ISSN  2075-2180. S2CID  418549.
  14. ^ Padovani, Luca (2017). "Простая библиотечная реализация бинарных сессий". Журнал функционального программирования . 27 : e4. doi : 10.1017/S0956796816000289. hdl : 2318/1634956 . ISSN  0956-7968. S2CID  19776781.
  15. ^ Имаи, Кейго; Ёсида, Нобуко; Юэн, Сёдзи (март 2019 г.). «Session-ocaml: библиотека на основе сеансов с полярностями и линзами». Science of Computer Programming . 172 : 135–159 . doi : 10.1016/j.scico.2018.08.005 . hdl : 10044/1/63748 . ISSN  0167-6423. S2CID  69673075.
  16. ^ Имаи, Кейго. "Session OCaml". www.ct.info.gifu-u.ac.jp . Получено 2 ноября 2021 г. .
  17. ^ Кокке, Вэнь; Дардха, Орнела (26 марта 2021 г.). «Типы сеансов без взаимоблокировок в линейном Haskell». arXiv : 2103.14481 [cs.PL].
  18. ^ "Проверка состояния типов Java". GitHub .
  19. ^ Баккиани, Лоренцо; Браветти, Марио; Джунти, Марко; Мота, Жуан; Равара, Антониу (2022). «Проверка состояния типов Java, поддерживающая наследование». наук. Вычислить. Программа . 221 : 102844. doi : 10.1016/j.scico.2022.102844 . hdl : 10362/145315 . S2CID  250940803.
  20. ^ Мота, Жуан; Джунти, Марко; Равара, Антониу (2021). «Проверка состояния типов Java». Материалы КООРДИНАЦИИ 2021 . Конспекты лекций по информатике. Том. 12717. С.  121–133 . doi :10.1007/978-3-030-78142-2_8. ISBN 978-3-030-78141-5. S2CID  235383301.
  21. ^ Рубичини, Алессио; Падовани, Лука (2023). «Swift Sessions: библиотечная реализация бинарных типов сеансов в Swift». GitHub .


Значок заглушки

Эта статья по информатике — заглушка . Вы можете помочь Википедии, расширив ее.

Получено с "https://en.wikipedia.org/w/index.php?title=Тип_сеанса&oldid=1237406775"