Семантики языков программирования 4 модуль 2019

Материал из CSC Wiki
Перейти к:навигация, поиск

Преподаватель -- Подкопаев Антон Викторович, anton@podkopaev.net

Оценивание

Разбалловка по системе ВШЭ:

  • 4 балла за домашние задания (на языке Coq);
  • 4 балла за устный экзамен;
  • 2 балла за активность на занятиях.

Репозиторий с заданием

https://classroom.github.com/a/Qse5BFEm

Материалы курса

Слайды: [часть 1] [Weak Memory]

Рекомендуемая книга: The Formal Semantics of Programming Languages, Glynn Winskel

Ресурсы по Coq

Coq tactics cheatsheets (краткая информация по тактикам):

1) http://www.inf.ed.ac.uk/teaching/courses/tspl/cheatsheet.pdf

2) https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html

Coq Reference Manual (полная информация по тактикам), https://coq.inria.fr/distrib/current/refman/

Software Foundations. Logical Foundations (классический "вводный" курс по Coq), https://softwarefoundations.cis.upenn.edu/lf-current/index.html

Необходимые библиотеки для Coq

С помощью opam (https://opam.ocaml.org) нужно установить библиотеки coq=8.8.2, bignums и hahn:

opam remote add coq-released https://coq.inria.fr/opam/released

opam remote add coq-weakmemory-local -k git https://github.com/weakmemory/local-coq-opam-archive

opam install coq coq-bignums coq-hahn

Темы вопросов на экзамен

1. Семантика большого и малого шагов для выражений. Эквивалентность выражений. Индукция по дереву выражения. Детерминированность семантик.

2. Индукция. Фундированное множество.

3. Семантика большого и малого шагов для утверждений (statements). Детерминированность семантик. Параллельная композиция и её семантика.

4. Аксиоматическая семантика. Правила Хоара и их корректность.

5. Слабые модели памяти. Операционные модели последовательной консистентности (SC) и полного порядка на записях (TSO).

6. Декларативные (аксиоматические) модели памяти. Понятие графа исполнения программы. SC, COH, RA, C11.

7. Связь между операционными и декларативными моделями SC и StrongCOH.