История изменений
Исправление AndreyKl, (текущая версия) :
о многопоточном коде можно рассуждать методом Овицки-Гриза (искать owicki-gries)
https://mediatum.ub.tum.de/doc/601717/601717.pdf
если к практике переходить, сейчас так же модно всё это как то сочетать например с тем что называется permission-based reasoning http://viper.ethz.ch/tutorial/#permissions
(хотя и в первом документе вполне себе практика)
прям если описать, то можно с помощью монады недетерминированного выбора например.
https://wiki.haskell.org/Nondeterminism,_monadically
ну конечно надо упомянуть конкурентрую логику с разделением
https://read.seas.harvard.edu/~kohler/class/cs260r-17/brookes16concurrent.pdf
короче тут вступление будет на академический час наверное..
Исправление AndreyKl, :
о многопоточном коде можно рассуждать методом Овицки-Гриза (искать owicki-gries)
https://mediatum.ub.tum.de/doc/601717/601717.pdf
если к практике переходить, сейчас так же модно всё это как то сочетать например с тем что называется permission-based reasoning http://viper.ethz.ch/tutorial/#permissions
(хотя и в первом документе вполне себе практика)
прям если описать, то можно с помощью монады недетерминированного выбора например.
https://wiki.haskell.org/Nondeterminism,_monadically
короче тут вступление будет на академический час наверное..
Исправление AndreyKl, :
о многопоточном коде можно рассуждать методом Овицки-Гриза (искать owicki-gries)
https://mediatum.ub.tum.de/doc/601717/601717.pdf
если к практике переходить, сейчас так же модно всё это как то сочетать например с тем что называется permission-based reasoning http://viper.ethz.ch/tutorial/#permissions
(хотя и в первом документе вполне себе практика)
прям если описать, то можно с помощью монады недетерминированного выбора например.
https://wiki.haskell.org/Nondeterminism,_monadically
короче да, вопросец ты задал...
Исправление AndreyKl, :
о многопоточном коде можно рассуждать методом Овицки-Гриза (искать owicki-gries)
https://mediatum.ub.tum.de/doc/601717/601717.pdf
если к практике переходить, сейчас можно всё это как то сочетать например с тем что называется permission-based reasoning http://viper.ethz.ch/tutorial/#permissions
прям если описать, то можно с помощью монады недетерминированного выбора например.
https://wiki.haskell.org/Nondeterminism,_monadically
короче да, вопросец ты задал...
Исходная версия AndreyKl, :
о многопоточном коде можно рассуждать методом Овицки-Гриза (искать owicki-gries)
https://mediatum.ub.tum.de/doc/601717/601717.pdf
всё это как то сочетают например с тем что называется permission-based reasoning http://viper.ethz.ch/tutorial/#permissions
прям если описать, то можно с помощью монады недетерминированного выбора например.
https://wiki.haskell.org/Nondeterminism,_monadically
короче да, вопросец ты задал...