{"id":405567,"date":"2024-06-29T18:24:01","date_gmt":"2024-06-29T18:24:01","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=405567"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=405567","title":{"rendered":"<span>\u041f\u0435\u0440\u0432\u044b\u0439 truly stateless \u043e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u0430 \u0438 \u0435\u0433\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u043d\u0430 Coq<\/span>"},"content":{"rendered":"<div><!--[--><!--]--><\/div>\n<div id=\"post-content-body\">\n<div>\n<div class=\"article-formatted-body article-formatted-body article-formatted-body_version-2\">\n<div xmlns=\"http:\/\/www.w3.org\/1999\/xhtml\">\n<p>\u041d\u0430\u0434\u043e\u0435\u043b\u0438 \u043d\u0435\u0441\u0442\u0430\u0431\u0438\u043b\u044c\u043d\u044b\u0435 \u0431\u0430\u0433\u0438 \u0432 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u043e\u043c \u043a\u043e\u0434\u0435? \u041f\u043e\u043f\u0440\u043e\u0431\u0443\u0439 \u0432\u043e\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c\u0441\u044f \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u0430\u043c\u0438! \u0412\u0435\u0434\u044c \u0431\u043e\u043b\u044c\u0448\u0435 \u043d\u0435 \u043d\u0430\u0434\u043e \u0431\u043e\u044f\u0442\u044c\u0441\u044f \u043d\u0435\u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0445 \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u043e\u0432,\u00a0 \u0440\u0430\u0431\u043e\u0442\u0430\u044e\u0449\u0438\u0445 \u043b\u0438\u0431\u043e \u0437\u0430 \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0432\u0440\u0435\u043c\u044f, \u043b\u0438\u0431\u043e \u043d\u0435\u043e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u043e. \u0412\u0441\u0435 \u044d\u0442\u043e \u0432 \u043f\u0440\u043e\u0448\u043b\u043e\u043c: \u0432 <a href=\"https:\/\/www.mpi-sws.org\/\"><u>Max Planck Institute for Software Systems<\/u><\/a> \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043b\u0438 \u043d\u043e\u0432\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u043e\u0434 \u043d\u0430\u0437\u0432\u0430\u043d\u0438\u0435\u043c TruSt, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0440\u0435\u0448\u0430\u0435\u0442 \u044d\u0442\u0438 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0438, \u043a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d \u043d\u0430 Coq.<\/p>\n<p>\u041c\u0435\u043d\u044f \u0437\u043e\u0432\u0443\u0442 \u0412\u043b\u0430\u0434\u0438\u043c\u0438\u0440 \u0413\u043b\u0430\u0434\u0448\u0442\u0435\u0439\u043d. \u042d\u0442\u0438\u043c \u043b\u0435\u0442\u043e\u043c \u044f \u043f\u0440\u043e\u0445\u043e\u0434\u0438\u043b \u0441\u0442\u0430\u0436\u0438\u0440\u043e\u0432\u043a\u0443 \u0432 MPI-SWS \u0432 \u0433\u0440\u0443\u043f\u043f\u0435, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u0440\u0438\u0434\u0443\u043c\u0430\u043b\u0430 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043d\u043e\u0432\u043e\u0433\u043e \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u0430 \u0434\u043b\u044f \u043f\u043e\u0438\u0441\u043a\u0430 \u0431\u0430\u0433\u043e\u0432 \u0432 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430\u0445. \u042d\u0442\u043e\u0442 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u044b\u043c \u0438 truly stateless (\u0432\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u0435 \u0447\u0435\u0433\u043e \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0441 \u043b\u0438\u043d\u0435\u0439\u043d\u044b\u043c\u0438 \u0437\u0430\u0442\u0440\u0430\u0442\u0430\u043c\u0438 \u043f\u043e \u043f\u0430\u043c\u044f\u0442\u0438). \u0412 \u044d\u0442\u043e\u043c \u043f\u043e\u0441\u0442\u0435 \u044f \u0440\u0430\u0441\u0441\u043a\u0430\u0436\u0443, \u043a\u0430\u043a \u0440\u0430\u0431\u043e\u0442\u0430\u044e\u0442 \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u044b, \u0432 \u043a\u0430\u043a\u0438\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445 \u0438\u0445 \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c, \u0438 \u0447\u0442\u043e \u0437\u0430 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0440\u0438\u0434\u0443\u043c\u0430\u043b\u0438 \u043c\u043e\u0438 \u043a\u043e\u043b\u043b\u0435\u0433\u0438. \u0410 \u0435\u0449\u0435 \u043a\u0430\u043a \u044f \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u043b \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0435\u0433\u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u043d\u0430 Coq.\u00a0<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w780q1\/getpro\/habr\/upload_files\/ec7\/5bd\/762\/ec75bd7620962fff310db64dc528c7dd.jpeg\" width=\"780\" height=\"440\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/ec7\/5bd\/762\/ec75bd7620962fff310db64dc528c7dd.jpeg\" data-blurred=\"true\"\/><figcaption><\/figcaption><\/figure>\n<h3>\u041e \u0441\u0435\u0431\u0435\u00a0<\/h3>\n<p>\u042f \u0443\u0447\u0443\u0441\u044c \u043d\u0430 4-\u043e\u043c \u043a\u0443\u0440\u0441\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u00ab\u041c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0430, \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u044b \u0438 \u0430\u043d\u0430\u043b\u0438\u0437 \u0434\u0430\u043d\u043d\u044b\u0445\u00bb \u0444\u0430\u043a\u0443\u043b\u044c\u0442\u0435\u0442\u0430 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0438 \u0438 \u043a\u043e\u043c\u043f\u044c\u044e\u0442\u0435\u0440\u043d\u044b\u0445 \u043d\u0430\u0443\u043a \u0421\u041f\u0431\u0413\u0423, \u0430 \u0442\u0430\u043a\u0436\u0435 \u0440\u0430\u0431\u043e\u0442\u0430\u044e \u0432 <a href=\"https:\/\/old.research.jetbrains.org\/ru\/groups\/plt_lab\"><u>\u041b\u0430\u0431\u043e\u0440\u0430\u0442\u043e\u0440\u0438\u0438 \u044f\u0437\u044b\u043a\u043e\u0432\u044b\u0445 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u0432<\/u><\/a> JetBrains Research. \u042f \u0431\u043e\u043b\u044c\u0448\u0435 \u0434\u0432\u0443\u0445 \u043b\u0435\u0442 \u0438\u0437\u0443\u0447\u0430\u044e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0443\u044e \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u0438 \u0432 \u043e\u0441\u043d\u043e\u0432\u043d\u043e\u043c \u043f\u0438\u0448\u0443 \u043d\u0430 \u044f\u0437\u044b\u043a\u0435 Coq.<\/p>\n<h3>\u041e \u0441\u0442\u0430\u0436\u0438\u0440\u043e\u0432\u043a\u0435<\/h3>\n<p>\u042d\u0442\u0438\u043c \u043b\u0435\u0442\u043e\u043c \u043c\u043d\u0435 \u043f\u043e\u0441\u0447\u0430\u0441\u0442\u043b\u0438\u0432\u0438\u043b\u043e\u0441\u044c \u043f\u0440\u043e\u0439\u0442\u0438 \u0441\u0442\u0430\u0436\u0438\u0440\u043e\u0432\u043a\u0443 \u0432 <a href=\"https:\/\/www.mpi-sws.org\/\"><u>Max Planck Institute for Software Systems<\/u><\/a>. \u041f\u043e\u043f\u0430\u043b \u044f \u0442\u0443\u0434\u0430 \u043d\u0435\u0441\u043b\u0443\u0447\u0430\u0439\u043d\u043e. \u0414\u0435\u043b\u043e \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u041b\u0430\u0431\u043e\u0440\u0430\u0442\u043e\u0440\u0438\u044f \u044f\u0437\u044b\u043a\u043e\u0432\u044b\u0445 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u0432 JBR \u0442\u0435\u0441\u043d\u043e \u0441\u043e\u0442\u0440\u0443\u0434\u043d\u0438\u0447\u0430\u0435\u0442 \u0441 \u044d\u0442\u0438\u043c \u0438\u043d\u0441\u0442\u0438\u0442\u0443\u0442\u043e\u043c. \u0412 \u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, \u0440\u0443\u043a\u043e\u0432\u043e\u0434\u0438\u0442\u0435\u043b\u044c \u043c\u043e\u0435\u0439 \u0433\u0440\u0443\u043f\u043f\u044b <a href=\"https:\/\/podkopaev.net\"><u>\u0410\u043d\u0442\u043e\u043d \u041f\u043e\u0434\u043a\u043e\u043f\u0430\u0435\u0432<\/u><\/a> \u0431\u044b\u043b \u043f\u043e\u0441\u0442\u0434\u043e\u043a\u043e\u043c \u0443 \u043f\u0440\u043e\u0444\u0435\u0441\u0441\u043e\u0440\u0430 MPI <a href=\"https:\/\/people.mpi-sws.org\/~viktor\/\"><u>\u0412\u0438\u043a\u0442\u043e\u0440\u0430 \u0412\u0430\u0444\u0435\u044f\u0434\u0438\u0441\u0430<\/u><\/a>. \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u0441 \u0440\u0435\u043a\u043e\u043c\u0435\u043d\u0434\u0430\u0446\u0438\u0435\u0439 \u043e\u0442 \u0410\u043d\u0442\u043e\u043d\u0430 \u043d\u0430 \u043c\u0435\u043d\u044f \u0431\u044b\u0441\u0442\u0440\u043e \u043e\u0431\u0440\u0430\u0442\u0438\u043b\u0438 \u0432\u043d\u0438\u043c\u0430\u043d\u0438\u0435 \u0438 \u0443\u0441\u0442\u0440\u043e\u0438\u043b\u0438 \u0441\u043e\u0431\u0435\u0441\u0435\u0434\u043e\u0432\u0430\u043d\u0438\u0435 \u0441 \u0412\u0438\u043a\u0442\u043e\u0440\u043e\u043c. \u0412 \u0438\u0442\u043e\u0433\u0435 \u043c\u0435\u043d\u044f \u0437\u0430\u0447\u0438\u0441\u043b\u0438\u043b\u0438 \u0441\u0442\u0430\u0436\u0435\u0440\u043e\u043c \u043d\u0430 \u0434\u0432\u0430 \u043c\u0435\u0441\u044f\u0446\u0430 \u2014 \u0441 \u0438\u044e\u043b\u044f \u043f\u043e \u0430\u0432\u0433\u0443\u0441\u0442 2021 \u0433\u043e\u0434\u0430. \u0421\u0442\u0430\u0436\u0438\u0440\u043e\u0432\u043a\u0430 \u043f\u0440\u043e\u0445\u043e\u0434\u0438\u043b\u0430 \u0434\u0438\u0441\u0442\u0430\u043d\u0446\u0438\u043e\u043d\u043d\u043e.<\/p>\n<h3>\u041e \u043f\u0440\u043e\u0435\u043a\u0442\u0435, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u044f \u0440\u0430\u0431\u043e\u0442\u0430\u043b<\/h3>\n<p>\u0412 \u043d\u0430\u0447\u0430\u043b\u0435 \u043b\u0435\u0442\u0430 \u043a\u043e\u043c\u0430\u043d\u0434\u0430 \u0432 MPI-SWS, \u043a \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u044f \u043f\u0440\u0438\u0441\u043e\u0435\u0434\u0438\u043d\u0438\u043b\u0441\u044f, \u0433\u043e\u0442\u043e\u0432\u0438\u043b\u0430\u0441\u044c \u043a \u043f\u043e\u0434\u0430\u0447\u0435 \u0441\u0442\u0430\u0442\u044c\u0438 \u043d\u0430 \u043a\u043e\u043d\u0444\u0435\u0440\u0435\u043d\u0446\u0438\u044e <a href=\"https:\/\/popl22.sigplan.org\/details\/POPL-2022-popl-research-papers\/49\/Truly-Stateless-Optimal-Dynamic-Partial-Order-Reduction\"><u>POPL<\/u><\/a>. \u0415\u0441\u043b\u0438 \u0432\u043a\u0440\u0430\u0442\u0446\u0435, \u043e\u043d\u0438 \u043f\u0440\u0438\u0434\u0443\u043c\u0430\u043b\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043d\u043e\u0432\u043e\u0433\u043e \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u0430 (\u0434\u0430\u043b\u0435\u0435 \u041c\u0421) \u0434\u043b\u044f \u043f\u043e\u0438\u0441\u043a\u0430 \u0431\u0430\u0433\u043e\u0432 \u0432 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430\u0445 \u0438 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u043b\u0438 \u043c\u043d\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0435\u0433\u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u043d\u0430 Coq. \u042d\u0442\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0435\u0439 \u044f \u0438 \u0437\u0430\u043d\u0438\u043c\u0430\u043b\u0441\u044f.<\/p>\n<p>\u041d\u043e \u0434\u0430\u0432\u0430\u0439\u0442\u0435 \u043e\u0431\u043e \u0432\u0441\u0435\u043c \u043f\u043e \u043f\u043e\u0440\u044f\u0434\u043a\u0443. \u041d\u0430\u0447\u043d\u0435\u043c \u0441 Coq.<\/p>\n<h3>O Coq<\/h3>\n<p>Coq \u2014 \u044d\u0442\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u0439 \u044f\u0437\u044b\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441 \u043e\u0447\u0435\u043d\u044c \u043c\u043e\u0449\u043d\u043e\u0439 \u0441\u0438\u0441\u0442\u0435\u043c\u043e\u0439 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432. \u0421 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043d\u0435\u0435 \u043f\u043e <a href=\"https:\/\/en.wikipedia.org\/wiki\/Curry%E2%80%93Howard_correspondence\"><u>\u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u044e \u041a\u0430\u0440\u0440\u0438-\u0413\u043e\u0432\u0430\u0440\u0434\u0430<\/u><\/a> \u0432 Coq \u0443\u0434\u0430\u0435\u0442\u0441\u044f \u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0438 \u043d\u0430 \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0442\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u043d \u0441\u043c\u043e\u0436\u0435\u0442 \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c. \u041f\u0440\u0438\u043c\u0435\u0440\u044b \u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u043e\u043a \u0442\u0435\u043e\u0440\u0435\u043c \u0432 Coq \u0443 \u043d\u0430\u0441 \u0435\u0449\u0435 \u0431\u0443\u0434\u0443\u0442, \u0430 \u043f\u043e\u043a\u0430, \u0447\u0442\u043e\u0431\u044b \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0442\u044c \u043e \u0447\u0435\u043c \u0440\u0435\u0447\u044c, \u043c\u043e\u0436\u043d\u043e \u043f\u043e\u0447\u0438\u0442\u0430\u0442\u044c \u043d\u0430\u0447\u0430\u043b\u043e <a href=\"https:\/\/habr.com\/ru\/post\/182442\/\"><u>\u043c\u044f\u0433\u043a\u043e\u0433\u043e \u0432\u0432\u0435\u0434\u0435\u043d\u0438\u044f<\/u><\/a>. \u0413\u043b\u0430\u0432\u043d\u043e\u0435, \u0447\u0442\u043e \u0442\u0443\u0442 \u043d\u0430\u0434\u043e \u043f\u043e\u043d\u044f\u0442\u044c \u2014 \u043d\u0430 \u044d\u0442\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u0442\u0435\u043e\u0440\u0435\u043c\u044b, \u0438 \u043e\u043d \u0435\u0433\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442. \u0421\u0440\u0435\u0434\u0438 CS \u0441\u043e\u043e\u0431\u0449\u0435\u0441\u0442\u0432\u0430 \u0441\u0447\u0438\u0442\u0430\u0435\u0442\u0441\u044f, \u0447\u0442\u043e \u0442\u0435\u043e\u0440\u0435\u043c\u044b, \u043f\u0440\u043e\u0432\u0435\u0440\u0435\u043d\u043d\u044b\u0435 \u043d\u0430 Coq, \u043d\u0435 \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u0442 \u043e\u0448\u0438\u0431\u043e\u043a \u0432 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430\u0445.\u00a0<\/p>\n<h3>\u041e \u0431\u0430\u0433\u0430\u0445 \u0432 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u043e\u043c \u043a\u043e\u0434\u0435\u00a0<\/h3>\n<p>\u0414\u0443\u043c\u0430\u044e \u0445\u0430\u0431\u0440\u043e\u0436\u0438\u0442\u0435\u043b\u0438 \u0437\u043d\u0430\u044e\u0442, \u0447\u0442\u043e \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u2014 \u044d\u0442\u043e \u0448\u0442\u0443\u043a\u0430 \u0441\u043b\u043e\u0436\u043d\u0430\u044f. \u0418\u043d\u043e\u0433\u0434\u0430 \u0432 \u043d\u0438\u0445 \u043f\u043e\u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u0431\u0430\u0433\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u0447\u0435\u043d\u044c \u0442\u044f\u0436\u0435\u043b\u043e \u043e\u0442\u043b\u043e\u0432\u0438\u0442\u044c \u0442\u0435\u0441\u0442\u0430\u043c\u0438. \u0422\u0430\u043a\u0438\u0435 \u0431\u0430\u0433\u0438 \u043c\u043e\u0433\u0443\u0442 \u043f\u043e\u044f\u0432\u043b\u044f\u0442\u044c\u0441\u044f \u043f\u0430\u0440\u0443 \u0440\u0430\u0437 \u043d\u0430 \u0442\u044b\u0441\u044f\u0447\u0443 \u0437\u0430\u043f\u0443\u0441\u043a\u043e\u0432 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u043e\u0434\u043d\u0430\u043a\u043e, \u0435\u0441\u043b\u0438 \u0435\u0439 \u0435\u0436\u0435\u0434\u043d\u0435\u0432\u043d\u043e \u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u043f\u043e\u0440\u044f\u0434\u043a\u0430 \u0434\u0435\u0441\u044f\u0442\u0438 \u0442\u044b\u0441\u044f\u0447 \u0447\u0435\u043b\u043e\u0432\u0435\u043a, \u0442\u043e \u0445\u043e\u0447\u0435\u0442\u0441\u044f \u043a\u0430\u043a-\u0442\u043e \u0431\u0430\u0433 \u043e\u0442\u043b\u043e\u0432\u0438\u0442\u044c \u0438 \u0438\u0441\u043f\u0440\u0430\u0432\u0438\u0442\u044c. \u041e\u0434\u043d\u0438\u043c \u0438\u0437 \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u043a\u0430\u043a \u0440\u0430\u0437 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f MC.<\/p>\n<p>\u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u0440\u0430\u0437\u0431\u0435\u0440\u0435\u043c \u043f\u0440\u0438\u043c\u0435\u0440 \u0442\u0430\u043a\u043e\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b. \u041f\u0440\u0438\u043c\u0435\u0440 \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u043e\u0431\u044a\u0435\u043c\u043d\u044b\u0439, \u043d\u043e \u043e\u043d \u043f\u043e\u043c\u043e\u0436\u0435\u0442 \u043f\u043e\u043d\u044f\u0442\u044c, \u0432 \u043a\u0430\u043a\u0438\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445 \u0440\u0430\u0437\u0443\u043c\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u044b. \u0415\u0441\u043b\u0438 \u0445\u043e\u0442\u0438\u0442\u0435 \u043f\u0440\u043e\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u043f\u0440\u0438\u043c\u0435\u0440, \u0436\u043c\u0438\u0442\u0435 <a href=\"#1\">\u0441\u044e\u0434\u0430<\/a>.<\/p>\n<p>\u041f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u044c\u0442\u0435 \u0441\u0435\u0431\u0435 \u043b\u044e\u0431\u0438\u043c\u044b\u0439 \u0431\u0430\u043d\u043a. \u0410 \u0442\u0435\u043f\u0435\u0440\u044c \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u044c\u0442\u0435, \u0447\u0442\u043e \u0432\u0430\u0441 \u043d\u0430\u0437\u043d\u0430\u0447\u0438\u043b\u0438 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0441\u0442\u043e\u043c \u0432 \u044d\u0442\u043e\u043c \u0431\u0430\u043d\u043a\u0435 \u0438 \u043f\u043e\u043f\u0440\u043e\u0441\u0438\u043b\u0438 \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043a\u043e\u0434 \u0434\u043b\u044f \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u044f \u043e\u0447\u0435\u0440\u0435\u0434\u0435\u0439. \u0427\u0435\u043b\u043e\u0432\u0435\u043a \u043f\u0440\u0438\u0445\u043e\u0434\u0438\u0442 \u0432 \u0431\u0430\u043d\u043a, \u0431\u0435\u0440\u0435\u0442 \u043d\u043e\u043c\u0435\u0440\u043e\u043a \u0438 \u0436\u0434\u0435\u0442 \u0441\u0432\u043e\u0435\u0439 \u043e\u0447\u0435\u0440\u0435\u0434\u0438.<\/p>\n<p>\u0423\u0441\u043b\u043e\u0432\u043d\u043e \u0432\u0430\u0448\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430 \u0434\u043e\u043b\u0436\u043d\u0430 \u0443\u043c\u0435\u0442\u044c:<\/p>\n<ol>\n<li>\n<p>\u0425\u0440\u0430\u043d\u0438\u0442\u044c \u043d\u043e\u043c\u0435\u0440 \u0431\u0438\u043b\u0435\u0442\u0438\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u0434\u0430\u043d \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u043c\u0443 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0443;<\/p>\n<\/li>\n<li>\n<p>\u0425\u0440\u0430\u043d\u0438\u0442\u044c \u043d\u043e\u043c\u0435\u0440 \u0431\u0438\u043b\u0435\u0442\u0430 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0441\u0435\u0439\u0447\u0430\u0441 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u044e\u0442;<\/p>\n<\/li>\n<li>\n<p>\u0412\u044b\u0434\u0430\u0432\u0430\u0442\u044c \u043d\u043e\u0432\u044b\u0435 \u0431\u0438\u043b\u0435\u0442\u044b;<\/p>\n<\/li>\n<li>\n<p>\u041c\u0435\u043d\u044f\u0442\u044c \u043d\u043e\u043c\u0435\u0440 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u044e\u0449\u0435\u0433\u043e\u0441\u044f \u0431\u0438\u043b\u0435\u0442\u0430.<\/p>\n<\/li>\n<\/ol>\n<p>\u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u043f\u043e\u043f\u0440\u043e\u0431\u0443\u0435\u043c \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u0442\u0430\u043a\u043e\u0435 \u043d\u0430 C, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u043e\u0441\u0442\u044c. \u0421\u043d\u0430\u0447\u0430\u043b\u0430 \u0437\u0430\u0432\u0435\u0434\u0435\u043c \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u0443, \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u044e\u0449\u0443\u044e \u043f\u0430\u043c\u044f\u0442\u044c \u043d\u0430\u0448\u0435\u0433\u043e \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0430 \u043f\u043e \u0432\u044b\u0434\u0430\u0447\u0435 \u0431\u0438\u043b\u0435\u0442\u043e\u0432:<\/p>\n<pre><code class=\"cpp\">struct ticketlock_s { atomic_int next; \/\/ \u043d\u043e\u043c\u0435\u0440 \u0431\u0438\u043b\u0435\u0442\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u0434\u0430\u043d \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u043c\u0443 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0443 atomic_int owner; \/\/ \u043d\u043e\u043c\u0435\u0440 \u0431\u0438\u043b\u0435\u0442\u0430 \u0443 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0441\u0435\u0439\u0447\u0430\u0441 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u044e\u0442  };<\/code><\/pre>\n<p>\u0422\u0430\u043a \u043a\u0430\u043a \u043c\u044b \u0431\u0443\u0434\u0435\u043c \u043f\u0438\u0441\u0430\u0442\u044c \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0439 \u043a\u043e\u0434, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u043f\u043e\u043b\u044f \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u044b \u0431\u0443\u0434\u0443\u0442 \u0448\u0430\u0440\u0438\u0442\u044c\u0441\u044f \u043c\u0435\u0436\u0434\u0443 \u043f\u043e\u0442\u043e\u043a\u0430\u043c\u0438, \u043d\u0430\u043c \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u0438\u0445 \u043d\u0435 \u043f\u0440\u043e\u0441\u0442\u043e int, a <a href=\"https:\/\/en.cppreference.com\/w\/c\/language\/atomic\"><u>atomic_int<\/u><\/a>.\u00a0<\/p>\n<p>\u0422\u0435\u043f\u0435\u0440\u044c \u0434\u0430\u0432\u0430\u0439\u0442\u0435 \u043e\u043f\u0438\u0448\u0435\u043c \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 \u0432\u044b\u0434\u0430\u0447\u0438 \u0431\u0438\u043b\u0435\u0442\u0430 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0443 \u0441 \u0435\u0433\u043e \u043f\u043e\u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0436\u0438\u0434\u0430\u043d\u0438\u0435\u043c \u0441\u0432\u043e\u0435\u0439 \u043e\u0447\u0435\u0440\u0435\u0434\u0438:<\/p>\n<pre><code class=\"cpp\">static inline void ticketlock_lock(struct ticketlock_s *l) {     int ticket = atomic_load(&amp;l->next); \/\/ \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u043d\u043e\u043c\u0435\u0440 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u0431\u0438\u043b\u0435\u0442\u0430     atomic_store(&amp;l->next, ticket + 1); \/\/ \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u0432\u0430\u0435\u043c \u043d\u043e\u043c\u0435\u0440 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u0431\u0438\u043b\u0435\u0442\u0430 \u043d\u0430 1     while (atomic_load(&amp;l->owner) != ticket) { \/\/ \u0447\u0435\u043b\u043e\u0432\u0435\u043a \u0436\u0434\u0435\u0442 \u0441\u0432\u043e\u0435\u0439 \u043e\u0447\u0435\u0440\u0435\u0434\u0438     } }<\/code><\/pre>\n<p>\u0422\u0435\u043f\u0435\u0440\u044c \u043c\u043e\u0436\u043d\u043e \u043e\u043f\u0438\u0441\u0430\u0442\u044c \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u0430 \u043e\u0447\u0435\u0440\u0435\u0434\u0438 \u043e\u0442 \u043e\u0434\u043d\u043e\u0433\u043e \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430 \u043a \u0434\u0440\u0443\u0433\u043e\u043c\u0443:<\/p>\n<pre><code class=\"cpp\">static inline void ticketlock_unlock(struct ticketlock_s *l) {     int owner = atomic_load(&amp;l->owner); \/\/ \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u043d\u043e\u043c\u0435\u0440 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0435\u043c\u043e\u0433\u043e \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430     atomic_store(&amp;l->owner, owner + 1); \/\/ \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u0432\u0430\u0435\u043c \u043d\u043e\u043c\u0435\u0440 }<\/code><\/pre>\n<p>\u0414\u043b\u044f \u043f\u0440\u043e\u0441\u0442\u043e\u0442\u044b \u0431\u0443\u0434\u0435\u043c \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u0435 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430 \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043e\u043d \u043a\u043b\u0430\u0434\u0435\u0442 \u043e\u0434\u043d\u0443 \u0434\u0435\u043d\u0435\u0436\u043a\u0443 \u043d\u0430 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0441\u0447\u0435\u0442 x, \u0430 \u043f\u043e\u0442\u043e\u043c \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430, \u0447\u0442\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435\u00a0 x \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u043b\u043e\u0441\u044c \u043d\u0430 \u043e\u0434\u0438\u043d:<\/p>\n<pre><code class=\"cpp\">int thread(void* unused) {      ticketlock_lock(&amp;lock); \/\/ \u0447\u0435\u043b\u043e\u0432\u0435\u043a \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u043d\u043e\u043c\u0435\u0440\u043e\u043a \u0438 \u0436\u0434\u0435\u0442      int y = x++; \/\/ \u0441\u043e\u0445\u0440\u0430\u043d\u044f\u0435\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 x \u0432 y \u0438 \u043a\u043b\u0430\u0434\u0435\u043c 1 \u0434\u0435\u043d\u0435\u0433 \u043d\u0430 x      assert(x == y + 1); \/\/ \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430, \u0447\u0442\u043e \u043d\u0430 x \u0431\u044b\u043b\u043e \u043f\u043e\u043b\u043e\u0436\u0435\u043d\u043e 1 \u0434\u0435\u043d\u0435\u0433      ticketlock_unlock(&amp;lock); \/\/ \u0437\u043e\u0432\u0435\u043c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e     return 0; }<\/code><\/pre>\n<p>\u041e\u0434\u043d\u0430\u043a\u043e \u043d\u0430\u0448 \u0431\u0430\u043d\u043a \u0434\u043e\u043b\u0436\u0435\u043d \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c \u043c\u043d\u043e\u0433\u043e \u043b\u044e\u0434\u0435\u0439, \u043f\u043e\u044d\u0442\u043e\u043c\u0443, \u0447\u0442\u043e\u0431\u044b \u0441\u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0435\u0433\u043e \u0440\u0430\u0431\u043e\u0442\u0443, \u043d\u0430\u0434\u043e \u0437\u0430\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 thread \u0432 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u0438\u0445 \u043f\u043e\u0442\u043e\u043a\u0430\u0445 \u043e\u0434\u043d\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u043e:<\/p>\n<pre><code class=\"cpp\">void test() {     ticketlock_init(&amp;lock); \/\/ \u0438\u043d\u0438\u0446\u0438\u0430\u043b\u0438\u0437\u0438\u0440\u0443\u0435\u043c \u043f\u043e\u043b\u044f \u043d\u0443\u043b\u044f\u043c\u0438       thrd_t threads[N_THREADS]; \/\/ \u0441\u043e\u0437\u0434\u0430\u0435\u043c \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u043f\u043e\u0442\u043e\u043a\u043e\u0432     for (int i = 0; i &lt; N_THREADS; ++i) {         int err = thrd_create(&amp;threads[i], thread, NULL); \/\/ \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u0435\u043c \u0432\u043e \u0432\u0441\u0435\u0445 \u043f\u043e\u0442\u043e\u043a\u0430\u0445 thread if (err) {   abort(); }     }      \/\/ \u0441\u043b\u0438\u0432\u0430\u0435\u043c \u043f\u043e\u0442\u043e\u043a\u0438     for (int i = 0; i &lt; N_THREADS; ++i) {         thrd_join(threads[i], NULL);     } }<\/code><\/pre>\n<p>\u041a\u0430\u043a \u043c\u044b \u0445\u043e\u0442\u0438\u043c, \u0447\u0442\u043e\u0431\u044b \u0440\u0430\u0431\u043e\u0442\u0430\u043b\u0430 \u043d\u0430\u0448\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430? \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043d\u0430 \u043f\u0440\u0438\u043c\u0435\u0440\u0435 \u0434\u0432\u0443\u0445 \u043f\u043e\u0442\u043e\u043a\u043e\u0432 (N_THREADS = 2).<\/p>\n<p>\u0411\u0443\u0434\u0435\u043c \u043f\u0440\u0438\u0434\u0435\u0440\u0436\u0438\u0432\u0430\u0442\u044c\u0441\u044f \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0430\u043c\u044f\u0442\u0438 Sequential Consistency (\u0442\u043e \u0435\u0441\u0442\u044c \u043c\u043e\u0436\u043d\u043e \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u043f\u0440\u0438 \u0437\u0430\u043f\u0443\u0441\u043a\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u0438 \u0440\u0430\u0437\u043d\u044b\u0445 \u043f\u043e\u0442\u043e\u043a\u043e\u0432 \u043f\u0435\u0440\u0435\u043c\u0435\u0448\u0438\u0432\u0430\u044e\u0442\u0441\u044f, \u0441\u043e\u0445\u0440\u0430\u043d\u044f\u044f \u0441\u0432\u043e\u0439 \u043f\u043e\u0440\u044f\u0434\u043e\u043a \u0432\u043d\u0443\u0442\u0440\u0438 \u043e\u0434\u043d\u043e\u0433\u043e \u043f\u043e\u0442\u043e\u043a\u0430, \u0438 \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u0435\u0442\u0441\u044f \u043e\u0434\u043d\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0439 \u043a\u043e\u0434).\u00a0<\/p>\n<p>\u0414\u043e\u043f\u0443\u0441\u0442\u0438\u043c \u0432 \u0431\u0430\u043d\u043a \u043f\u0440\u0438\u0448\u043b\u0438 \u041f\u0435\u0442\u044f (\u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a) \u0438 \u0412\u0430\u0441\u044f (\u0432\u0442\u043e\u0440\u043e\u0439 \u043f\u043e\u0442\u043e\u043a). \u0412 \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0441\u0438\u0442\u0443\u0430\u0446\u0438\u0438 \u043e\u043d\u0438 \u043d\u0430\u0445\u043e\u0434\u044f\u0442\u0441\u044f \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u043d\u0430 \u0441\u0442\u0440\u043e\u043a\u0435:<\/p>\n<pre><code class=\"cpp\">ticketlock_lock(&amp;lock);<\/code><\/pre>\n<p>\u041f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0438\u043c, \u0447\u0442\u043e \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a (\u0442\u043e \u0435\u0441\u0442\u044c \u041f\u0435\u0442\u044f \u043f\u0435\u0440\u0432\u044b\u0439 \u0432\u0437\u044f\u043b \u0431\u0438\u043b\u0435\u0442\u0438\u043a):<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next);     atomic_store(&amp;l->next, ticket + 1)<\/code><\/pre>\n<p>\u041e\u043d \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u0431\u0438\u043b\u0435\u0442 \u043d\u043e\u043c\u0435\u0440 0, \u0438 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0431\u0438\u043b\u0435\u0442 \u0431\u0443\u0434\u0435\u0442 \u0443\u0436\u0435 \u0438\u043c\u0435\u0442\u044c \u043d\u043e\u043c\u0435\u0440 1. \u041f\u043e\u0442\u043e\u043c, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0441\u044e\u0434\u0430 \u043c\u043e\u0436\u0435\u0442 \u0432\u0441\u0442\u0440\u043e\u0438\u0442\u044c\u0441\u044f \u0412\u0430\u0441\u0438\u043d (\u0432\u0442\u043e\u0440\u043e\u0439) \u043f\u043e\u0442\u043e\u043a \u0438 \u043e\u0442\u0442\u0443\u0434\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u0442\u0441\u044f \u0442\u0440\u0438 \u0441\u0442\u0440\u043e\u0447\u043a\u0438 (\u0412\u0430\u0441\u044f \u0432\u043e\u0437\u044c\u043c\u0435\u0442 \u0441\u0432\u043e\u0439 \u0431\u0438\u043b\u0435\u0442 \u0438 \u0441\u044f\u0434\u0435\u0442 \u0432 \u043e\u0447\u0435\u0440\u0435\u0434\u044c):<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next); \/\/ \u0412\u0430\u0441\u044f \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u0431\u0438\u043b\u0435\u0442 \u043d\u043e\u043c\u0435\u0440 1 atomic_store(&amp;l->next, ticket + 1); \/\/ \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0431\u0438\u043b\u0435\u0442 \u0442\u0435\u043f\u0435\u0440\u044c \u0438\u043c\u0435\u0435\u0442 \u043d\u043e\u043c\u0435\u0440 2 while (atomic_load(&amp;l->owner) != ticket) { \/\/ owner \u0440\u0430\u0432\u0435\u043d 0, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0412\u0430\u0441\u044f \u0436\u0434\u0435\u0442, \u043f\u043e\u043a\u0430 \u043d\u0435 \u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0438\u0442 \u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c \u041f\u0435\u0442\u0438\u043d \u043f\u043e\u0442\u043e\u043a }<\/code><\/pre>\n<p>\u041d\u0430\u043a\u043e\u043d\u0435\u0446 \u0432\u0441\u0442\u0440\u0430\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a: \u041f\u0435\u0442\u044f \u0441\u043f\u043e\u043a\u043e\u0439\u043d\u043e \u043f\u0435\u0440\u0435\u0441\u043a\u0430\u043a\u0438\u0432\u0430\u0435\u0442 \u0431\u0435\u0441\u043a\u043e\u043d\u0435\u0447\u043d\u044b\u0439 \u0446\u0438\u043a\u043b (\u0430 \u043d\u0435 \u0441\u0430\u0434\u0438\u0442\u0441\u044f \u0442\u0443\u0434\u0430 \u0436\u0434\u0430\u0442\u044c), \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u043d\u043e\u043c\u0435\u0440 \u0435\u0433\u043e \u0431\u0438\u043b\u0435\u0442\u0430 \u0441\u043e\u0432\u043f\u0430\u0434\u0430\u0435\u0442 \u0441 \u043d\u043e\u043c\u0435\u0440\u043e\u043c \u0431\u0438\u043b\u0435\u0442\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0443\u0442 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c.<\/p>\n<pre><code class=\"cpp\"> while (atomic_load(&amp;l->owner) != ticket) { \/\/ \u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u043d\u0435 \u0441\u0440\u0430\u0431\u0430\u0442\u044b\u0432\u0430\u0435\u0442, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e owner = 0, \u0430 \u0443 \u041f\u0435\u0442\u0438 \u043a\u0430\u043a \u0440\u0430\u0437 \u0431\u0438\u043b\u0435\u0442 \u043d\u043e\u043c\u0435\u0440 0  }<\/code><\/pre>\n<p>\u0414\u0430\u043b\u0435\u0435 \u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a \u0432\u044b\u0445\u043e\u0434\u0438\u0442 \u0438\u0437 <code>ticket_lock<\/code> \u0438 \u043d\u0430\u0447\u0438\u043d\u0430\u0435\u0442\u0441\u044f \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u0435 \u041f\u0435\u0442\u0438:<\/p>\n<pre><code class=\"cpp\">int y = x++; \/\/ \u041f\u0435\u0442\u044f \u043f\u043e\u043b\u043e\u0436\u0438\u043b \u0434\u0435\u043d\u0435\u0436\u043a\u0443 \u043d\u0430 \u0441\u0447\u0435\u0442 x assert(x == y + 1); \/\/ \u0432\u0441\u0435 \u0445\u043e\u0440\u043e\u0448\u043e: x = 1, y = 0  ticketlock_unlock(&amp;lock); \/\/ \u0437\u043e\u0432\u0435\u043c \u0412\u0430\u0441\u044e<\/code><\/pre>\n<p>\u0422\u0443\u0442 \u0412\u0430\u0441\u0438\u043d \u043f\u043e\u0442\u043e\u043a \u043d\u0435 \u043c\u043e\u0436\u0435\u0442 \u043d\u0438\u043a\u0443\u0434\u0430 \u0432\u0441\u0442\u0440\u043e\u0438\u0442\u044c\u0441\u044f \u0434\u043e \u0442\u043e\u0433\u043e, \u043a\u0430\u043a \u043c\u044b \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c <code>ticketlock_unlock(&amp;lock)<\/code>, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u043f\u043e\u043a\u0430 \u0432 \u041f\u0435\u0442\u0438\u043d\u043e\u043c \u043f\u043e\u0442\u043e\u043a\u0435 \u043d\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u0442\u0441\u044f <code>ticketlock_unlock(&amp;lock)<\/code>, \u043d\u043e\u043c\u0435\u0440 \u0412\u0430\u0441\u0438\u043d\u043e\u0433\u043e \u0431\u0438\u043b\u0435\u0442\u0430 (1) \u043d\u0435 \u0441\u043e\u0432\u043f\u0430\u0434\u0435\u0442 \u0441 \u043d\u043e\u043c\u0435\u0440\u043e\u043c \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0435\u043c\u043e\u0433\u043e \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430 (0), \u0438 \u0412\u0430\u0441\u044f \u043d\u0435 \u0441\u043c\u043e\u0436\u0435\u0442 \u0432\u044b\u0439\u0442\u0438 \u0438\u0437 \u0446\u0438\u043a\u043b\u0430 . \u0422\u0430\u043a\u0436\u0435 \u044f\u0441\u043d\u043e, \u0447\u0442\u043e <code>assert<\/code> \u043d\u0435 \u043d\u0430\u0440\u0443\u0448\u0438\u0442\u0441\u044f, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u041f\u0435\u0442\u044f \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 <code>x<\/code> (\u0442\u0430\u043c \u0431\u0443\u0434\u0435\u0442 1, \u0430 \u0432 y \u2014 0), \u043f\u043e\u0442\u043e\u043c \u0442\u043e \u0436\u0435 \u0441\u0430\u043c\u043e\u0435 \u0441\u0434\u0435\u043b\u0430\u0435\u0442 \u0412\u0430\u0441\u044f.<\/p>\n<p>\u042d\u0442\u043e \u0445\u043e\u0440\u043e\u0448\u0435\u0435 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u0442\u0430\u043a \u043a\u0430\u043a \u0445\u043e\u0442\u044c \u043f\u043e\u0442\u043e\u043a\u0438 \u0438 \u0438\u0441\u043f\u043e\u043b\u043d\u044f\u044e\u0442\u0441\u044f \u043f\u0430\u0440\u0430\u043b\u043b\u0435\u043b\u044c\u043d\u043e, \u043c\u044b \u043d\u0435 \u043c\u043e\u0436\u0435\u043c \u043d\u0430\u0447\u0430\u0442\u044c \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c \u0412\u0430\u0441\u044e, \u043f\u043e\u043a\u0430 \u043d\u0435 \u0437\u0430\u043a\u043e\u043d\u0447\u0438\u043c \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c \u041f\u0435\u0442\u044e.\u00a0<\/p>\n<p>\u0422\u0435\u043f\u0435\u0440\u044c \u0432\u043e\u043f\u0440\u043e\u0441: \u043c\u043e\u0436\u0435\u0442 \u043b\u0438 \u043a\u043e\u0433\u0434\u0430-\u0442\u043e \u043d\u0430\u0440\u0443\u0448\u0438\u0442\u0441\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c\u044b\u0439 <code>assert<\/code>? \u0418 \u043e\u0442\u0432\u0435\u0442: \u043a \u0441\u043e\u0436\u0430\u043b\u0435\u043d\u0438\u044e, \u0434\u0430. \u041d\u0430 \u0441\u0430\u043c\u043e\u043c \u0434\u0435\u043b\u0435 \u044d\u0442\u043e\u0442 <code>assert<\/code> \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f \u0440\u043e\u0432\u043d\u043e \u0442\u043e\u0433\u0434\u0430, \u043a\u043e\u0433\u0434\u0430 \u0432 \u043f\u0440\u043e\u0446\u0435\u0441\u0441 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u044f \u043e\u0434\u043d\u043e\u0433\u043e \u043a\u043b\u0438\u0435\u043d\u0442\u0430 \u0432\u0441\u0442\u0440\u0430\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u0435 \u0434\u0440\u0443\u0433\u043e\u0433\u043e. \u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u043f\u043e\u0441\u043c\u043e\u0442\u0440\u0438\u043c, \u043a\u0430\u043a \u044d\u0442\u043e \u043c\u043e\u0436\u0435\u0442 \u043f\u0440\u043e\u0438\u0437\u043e\u0439\u0442\u0438 \u0432 \u0441\u043b\u0443\u0447\u0430\u0435, \u0435\u0441\u043b\u0438 \u0443 \u043d\u0430\u0441 \u0434\u0432\u0430 \u043f\u043e\u0442\u043e\u043a\u0430.<\/p>\n<p>\u041f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0438\u043c \u0442\u0435\u043f\u0435\u0440\u044c, \u0447\u0442\u043e \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u0432 \u043f\u0435\u0440\u0432\u043e\u043c \u043f\u043e\u0442\u043e\u043a\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u043f\u0435\u0440\u0432\u0430\u044f \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f \u00a0<code>ticketlock_lock<\/code>:<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next);  \/\/ \u041f\u0435\u0442\u044f \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u0431\u0438\u043b\u0435\u0442 \u0441 \u043d\u043e\u043c\u0435\u0440\u043e\u043c 0<\/code><\/pre>\n<p>\u041f\u043e\u0442\u043e\u043c \u0441\u0440\u0430\u0437\u0443 \u0432\u043c\u0435\u0448\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u0432\u0442\u043e\u0440\u043e\u0439 \u043f\u043e\u0442\u043e\u043a, \u0438 \u0442\u0430\u043c \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u044e\u0442\u0441\u044f \u043f\u0435\u0440\u0432\u044b\u0435 \u0434\u0432\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u0438:<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next); \/\/ \u0412\u0430\u0441\u044f \u0442\u043e\u0436\u0435 \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u0431\u0438\u043b\u0435\u0442 \u0441 \u043d\u043e\u043c\u0435\u0440\u043e\u043c 0 atomic_store(&amp;l->next, ticket + 1); \/\/ \u043d\u043e\u043c\u0435\u0440 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u043d\u043e\u043c\u0435\u0440\u0430 \u0442\u0435\u043f\u0435\u0440\u044c 1<\/code><\/pre>\n<p>\u041d\u0430\u043a\u043e\u043d\u0435\u0446, \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0430\u044f \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u043f\u043e\u0442\u043e\u043a\u0430:<\/p>\n<pre><code class=\"cpp\">atomic_store(&amp;l->next, ticket + 1); \/\/ \u0432 \u043d\u043e\u043c\u0435\u0440 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u043f\u043e\u0442\u043e\u043a\u0430  \u0441\u043d\u043e\u0432\u0430 \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u0442\u0441\u044f 1<\/code><\/pre>\n<p>\u0414\u0430\u043b\u0435\u0435 \u043d\u0438 \u043e\u0434\u0438\u043d \u0438\u0437 \u043f\u043e\u0442\u043e\u043a\u043e\u0432 \u043d\u0435 \u0437\u0430\u0432\u0438\u0441\u0430\u0435\u0442 \u0432 \u0446\u0438\u043a\u043b\u0435 while, \u0438 \u043e\u043d\u0438 \u043e\u0431\u0430 \u0432\u044b\u0445\u043e\u0434\u044f\u0442 \u0438\u0437 <code>ticketlock_lock<\/code>. \u042d\u0442\u043e \u043f\u043b\u043e\u0445\u043e, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0442\u0435\u043f\u0435\u0440\u044c \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u0441\u043b\u0443\u0447\u0430\u0439\u043d\u043e \u043d\u0430\u0447\u0430\u0442\u044c \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c \u0438\u0445 \u043e\u0434\u043d\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u043e, \u0430 \u044d\u0442\u043e \u0438\u043d\u043e\u0433\u0434\u0430 \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 \u043a \u0440\u0430\u0437\u043d\u043e\u0433\u043e \u0440\u043e\u0434\u0430 \u043e\u0448\u0438\u0431\u043a\u0430\u043c (\u0432 \u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, \u043d\u0430\u0440\u0443\u0448\u0435\u043d\u0438\u044f <code>assert<\/code>\u2019a).<\/p>\n<p>\u0421\u043e\u0431\u044b\u0442\u0438\u044f \u043c\u043e\u0433\u0443\u0442 \u0440\u0430\u0437\u0432\u0438\u0432\u0430\u0442\u044c\u0441\u044f \u043a\u0430\u043a-\u0442\u043e \u0442\u0430\u043a: \u0441\u043d\u0430\u0447\u0430\u043b\u0430, \u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a \u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0430\u0435\u0442<\/p>\n<pre><code class=\"cpp\">int y = x++; \/\/ \u041f\u0435\u0442\u044f \u043f\u043e\u043b\u043e\u0436\u0438\u043b \u0434\u0435\u043d\u0435\u0436\u043a\u0443 \u043d\u0430 \u0441\u0447\u0435\u0442 x<\/code><\/pre>\n<p>\u0422\u0443\u0442 \u0441\u0440\u0430\u0437\u0443 \u0432\u0441\u0442\u0440\u043e\u0438\u043b\u0441\u044f \u0412\u0430\u0441\u044f:<\/p>\n<pre><code class=\"cpp\">int y = x++; \/\/ \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u043b\u0438 \u0412\u0430\u0441\u044e: \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u043b\u0438 x<\/code><\/pre>\n<p>\u0418 \u0432 \u0438\u0442\u043e\u0433\u0435 \u0432 \u043f\u0435\u0440\u0432\u043e\u043c \u043f\u043e\u0442\u043e\u043a\u0435 \u0432 y \u043d\u0430\u0445\u043e\u0434\u0438\u0442\u0441\u044f 0, \u0430 \u0445 \u0443\u0436\u0435 \u0440\u0430\u0432\u0435\u043d 2, \u0447\u0442\u043e \u0432\u0435\u0434\u0435\u0442 \u043a \u043d\u0435\u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044e <code>assert<\/code>\u2019a.<\/p>\n<p>\u042f\u0441\u043d\u043e, \u0447\u0442\u043e \u0442\u0443\u0442 \u0432\u043e\u0437\u043d\u0438\u043a\u043b\u0430 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0430, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0412\u0430\u0441\u044f \u043f\u043e\u043b\u0443\u0447\u0438\u043b \u0441\u0432\u043e\u0439 \u0431\u0438\u043b\u0435\u0442 \u0434\u043e \u0442\u043e\u0433\u043e, \u043a\u0430\u043a \u043d\u0430\u0448\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430 \u0443\u0441\u043f\u0435\u043b\u0430 \u0434\u043e \u043a\u043e\u043d\u0446\u0430 \u043e\u0431\u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u0438\u0435 \u0431\u0438\u043b\u0435\u0442\u0430 \u041f\u0435\u0442\u0435\u0439. \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u0447\u0442\u043e\u0431\u044b \u0435\u0435 \u0440\u0435\u0448\u0438\u0442\u044c, \u043d\u0430\u0434\u043e \u043f\u0440\u043e\u0441\u0442\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u0442\u0430\u043a, \u0447\u0442\u043e\u0431\u044b \u043e\u0434\u0438\u043d \u043f\u043e\u0442\u043e\u043a \u043d\u0435 \u043c\u043e\u0433 \u0432\u043b\u0435\u0437\u0442\u044c \u043c\u0435\u0436\u0434\u0443 \u0434\u0432\u0443\u043c\u044f \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f\u043c\u0438, \u043e\u0442\u0432\u0435\u0447\u0430\u044e\u0449\u0438\u043c\u0438 \u0437\u0430 \u0432\u044b\u0434\u0430\u0447\u0443 \u0431\u0438\u043b\u0435\u0442\u0430, \u043f\u043e\u043a\u0430 \u0438\u0445 \u0438\u0441\u043f\u043e\u043b\u043d\u044f\u0435\u0442 \u0434\u0440\u0443\u0433\u043e\u0439 \u043f\u043e\u0442\u043e\u043a. \u0410 \u0438\u043c\u0435\u043d\u043d\u043e:<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next); atomic_store(&amp;l->next, ticket + 1);<\/code><\/pre>\n<p>\u0414\u043b\u044f \u044d\u0442\u043e\u0433\u043e \u043c\u043e\u0436\u043d\u043e \u0438\u0445 \u043e\u0431\u044a\u0435\u0434\u0438\u043d\u0438\u0442\u044c \u0432 \u043e\u0434\u043d\u0443 \u0430\u0442\u043e\u043c\u0430\u0440\u043d\u0443\u044e \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044e:<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_fetch_add(&amp;l->next, 1);<\/code><\/pre>\n<p>\u00ab\u041f\u043b\u043e\u0445\u043e\u0439\u00bb \u0441\u043f\u043e\u0441\u043e\u0431 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0440\u0435\u0434\u043a\u043e, \u0442\u0430\u043a \u0447\u0442\u043e \u0442\u0435\u0441\u0442\u0430\u043c\u0438 \u0435\u0433\u043e \u043e\u0442\u043b\u043e\u0432\u0438\u0442\u044c \u043d\u0435\u043f\u0440\u043e\u0441\u0442\u043e. \u0418\u043c\u0435\u043d\u043d\u043e \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0442\u0443\u0442 \u043d\u0443\u0436\u0435\u043d \u043a\u0430\u043a\u043e\u0439-\u043d\u0438\u0431\u0443\u0434\u044c \u0434\u0440\u0443\u0433\u043e\u0439 \u043f\u0443\u0442\u044c \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0435\u0435 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438. <\/p>\n<p><a class=\"anchor\" name=\"1\" id=\"1\"><\/a><\/p>\n<h3>\u041e Model Checker<\/h3>\n<p>\u0427\u0442\u043e\u0431\u044b \u043b\u043e\u0432\u0438\u0442\u044c \u0442\u0430\u043a\u0438\u0435 \u0431\u0430\u0433\u0438, \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c MC. \u0427\u0442\u043e \u043e\u043d\u0438 \u0434\u0435\u043b\u0430\u044e\u0442? \u042d\u0442\u043e \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043d\u0430 \u0432\u0445\u043e\u0434 \u0431\u0435\u0440\u0443\u0442 \u0432\u0430\u0448 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0439 \u043a\u043e\u0434 \u0438 \u0441\u0442\u0430\u0440\u0430\u044e\u0442\u0441\u044f \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u043c \u0441\u043f\u043e\u0441\u043e\u0431\u043e\u043c \u043e\u0431\u043e\u0439\u0442\u0438 \u0432\u0441\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u0441\u0446\u0435\u043d\u044b \u0435\u0433\u043e \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f (\u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043f\u043e \u043c\u043e\u0434\u0443\u043b\u044e \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u044d\u043a\u0432\u0438\u0432\u0430\u043b\u0435\u043d\u0442\u043d\u043e\u0441\u0442\u0438). \u0414\u043b\u044f \u0442\u043e\u0433\u043e \u0447\u0442\u043e\u0431\u044b \u043f\u043e\u043d\u044f\u0442\u044c, \u043a\u0430\u043a \u043e\u043d\u0438 \u0440\u0430\u0431\u043e\u0442\u0430\u044e\u0442, \u0434\u0430\u0432\u0430\u0439\u0442\u0435 \u043e\u0431\u0440\u0430\u0442\u0438\u043c\u0441\u044f \u043a \u0441\u0435\u043c\u0430\u043d\u0442\u0438\u043a\u0435 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c.<\/p>\n<h3>\u041e \u0441\u0435\u043c\u0430\u043d\u0442\u0438\u043a\u0435 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c<\/h3>\n<p>\u041a\u0430\u0436\u0434\u043e\u0439 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u043e\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435 \u043c\u043e\u0436\u043d\u043e \u043f\u043e\u0441\u0442\u0430\u0432\u0438\u0442\u044c \u0432 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0435 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u00ab\u0433\u0440\u0430\u0444 \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f\u00bb. \u041a\u0430\u0436\u0434\u044b\u0439 \u0442\u0430\u043a\u043e\u0439 \u0433\u0440\u0430\u0444 \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u0442 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u043e\u0435 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u0432\u0435\u0434\u0443\u0449\u0438\u0445 \u043a \u043e\u0434\u043d\u043e\u043c\u0443 \u0438 \u0442\u043e\u043c\u0443 \u0436\u0435 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0443. \u0422\u043e \u0435\u0441\u0442\u044c \u0435\u0441\u043b\u0438 \u0443 \u0432\u0430\u0441 \u0435\u0441\u0442\u044c \u043d\u0430 \u0440\u0443\u043a\u0430\u0445 \u0442\u0430\u043a\u043e\u0439 \u0433\u0440\u0430\u0444, \u0432\u044b \u043c\u043e\u0436\u0435\u0442\u0435 \u00ab\u043f\u043e\u0447\u0442\u0438\u00bb \u0441\u043a\u0430\u0437\u0430\u0442\u044c, \u043a\u0430\u043a \u0438\u0441\u043f\u043e\u043b\u043d\u0438\u043b\u0430\u0441\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430, \u043d\u043e \u044d\u0442\u043e\u0433\u043e \u00ab\u043f\u043e\u0447\u0442\u0438\u00bb \u0445\u0432\u0430\u0442\u0430\u0435\u0442, \u0447\u0442\u043e\u0431\u044b \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440 \u043f\u043e\u043d\u044f\u0442\u044c, \u043d\u0430\u0440\u0443\u0448\u0430\u043b\u0438\u0441\u044c \u043b\u0438 \u043a\u0430\u043a\u0438\u0435-\u0442\u043e assert\u2019\u044b \u0438\u043b\u0438 \u043d\u0435\u0442.<\/p>\n<p>\u041f\u0440\u0438\u043c\u0435\u0440: \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0443 \u043d\u0430 \u043d\u0435\u043a\u043e\u043c \u043f\u0441\u0435\u0432\u0434\u043e\u044f\u0437\u044b\u043a\u0435:<\/p>\n<pre><code>    x := 0 x:= 1 || x:= 2     r := x    assert (r!=1)<\/code><\/pre>\n<p>\u0422\u0443\u0442 \u043c\u044b \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u043c \u0432 <code>x<\/code> 0, \u043f\u043e\u0442\u043e\u043c \u0432 \u0434\u0432\u0443\u0445 \u0440\u0430\u0437\u043d\u044b\u0445 \u043f\u043e\u0442\u043e\u043a\u0430\u0445 \u043f\u0438\u0448\u0435\u043c 1 \u0438 2, \u0438 \u0432 \u043a\u043e\u043d\u0446\u0435 \u0447\u0438\u0442\u0430\u0435\u043c \u0438\u0437 <code>x<\/code>.<\/p>\n<p>\u042d\u0442\u043e\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u00ab\u0433\u0440\u0430\u0444\u043e\u0432 \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f\u00bb. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0442\u0430\u043a\u043e\u0439:<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/893\/127\/429\/8931274297de4f7d7be3e8fd638eb831.png\" width=\"943\" height=\"465\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/893\/127\/429\/8931274297de4f7d7be3e8fd638eb831.png\"\/><figcaption><\/figcaption><\/figure>\n<p>\u0412 \u044d\u0442\u043e\u043c \u0433\u0440\u0430\u0444\u0435 \u0435\u0441\u0442\u044c \u0434\u0432\u0430 \u0442\u0438\u043f\u0430 \u0432\u0435\u0440\u0448\u0438\u043d, \u043e\u043d\u0438 \u043d\u0430\u0437\u044b\u0432\u0430\u044e\u0442\u0441\u044f \u0441\u043e\u0431\u044b\u0442\u0438\u044f\u043c\u0438:\u00a0<\/p>\n<ol>\n<li>\n<p><code>W(x,i)<\/code> \u2014 \u0437\u0430\u043f\u0438\u0441\u044c \u0432 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0443\u044e x \u0447\u0438\u0441\u043b\u0430 i (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u0438 <code>x := 0<\/code> \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 <code>W(x,0)<\/code>);<\/p>\n<\/li>\n<li>\n<p><code>R(x,j)<\/code> \u2014 \u0447\u0442\u0435\u043d\u0438\u0435 \u0438\u0437 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 x \u0447\u0438\u0441\u043b\u0430 j (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0435\u0441\u043b\u0438 \u043c\u044b \u0432 <code>r := x<\/code> \u043f\u0440\u043e\u0447\u0438\u0442\u0430\u043b\u0438 2, \u0442\u043e \u044d\u0442\u043e\u043c\u0443 \u0431\u0443\u0434\u0435\u0442 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u043e\u0432\u0430\u0442\u044c R(x,2)).<\/p>\n<\/li>\n<\/ol>\n<p>\u0418 \u0434\u0432\u0430 \u0442\u0438\u043f\u0430 \u0440\u0435\u0431\u0435\u0440:<\/p>\n<ol>\n<li>\n<p>\u0421\u0435\u0440\u044b\u0435 \u2014 program order. \u041e\u043d\u0438 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u044e\u0442 \u043f\u043e\u0440\u044f\u0434\u043a\u0443 \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u0439 (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440 x:=1 \u0438\u0434\u0435\u0442 \u043f\u043e\u0441\u043b\u0435 x:=0, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043c\u0435\u0436\u0434\u0443 \u043d\u0438\u043c\u0438 \u0441\u0442\u043e\u0438\u0442 \u0441\u0442\u0440\u0435\u043b\u043a\u0430);\u00a0<\/p>\n<\/li>\n<li>\n<p>\u0417\u0435\u043b\u0435\u043d\u044b\u0435 \u2014 reads from. \u041e\u043d\u0438 \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u044e\u0442, \u043e\u0442\u043a\u0443\u0434\u0430 \u0441\u043e\u0431\u044b\u0442\u0438\u0435 \u0447\u0442\u0435\u043d\u0438\u044f \u0431\u0435\u0440\u0435\u0442 \u0441\u0432\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 (\u0432 \u0434\u0430\u043d\u043d\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435\u0442\u00a0 r := x \u0447\u0438\u0442\u0430\u0435\u0442 \u0438\u0437 x:= 2).<\/p>\n<\/li>\n<\/ol>\n<p>\u0421\u043c\u043e\u0442\u0440\u044f \u043d\u0430 \u044d\u0442\u043e\u0442 \u0433\u0440\u0430\u0444, \u043b\u0435\u0433\u043a\u043e \u043f\u043e\u043d\u044f\u0442\u044c, \u0447\u0442\u043e <code>assert<\/code> \u043d\u0435 \u0441\u0440\u0430\u0431\u0430\u0442\u044b\u0432\u0430\u0435\u0442.<\/p>\n<h4>\u041e \u043c\u043e\u0434\u0435\u043b\u044f\u0445 \u043f\u0430\u043c\u044f\u0442\u0438<\/h4>\n<p>\u0417\u0430\u043f\u0443\u0441\u043a\u0430\u044f \u043e\u0434\u0438\u043d \u0438 \u0442\u043e\u0442 \u0436\u0435 \u043a\u043e\u0434 \u043d\u0430 \u0440\u0430\u0437\u043d\u044b\u0445 \u044f\u0437\u044b\u043a\u0430\u0445 \u0438\u043b\u0438 \u043d\u0430 \u0440\u0430\u0437\u043d\u044b\u0445 \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u043e\u0440\u0430\u0445, \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043d\u0430\u0431\u043b\u044e\u0434\u0430\u0442\u044c \u0440\u0430\u0437\u043d\u044b\u0435 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u044f. \u041f\u043e\u0447\u0435\u043c\u0443 \u0442\u0430\u043a \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442? \u0414\u0435\u043b\u043e \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043d\u0430\u0434 \u0432\u0430\u0448\u0438\u043c \u043a\u043e\u0434\u043e\u043c \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440, \u0430 \u043f\u043e\u0442\u043e\u043c \u0438 \u0441\u0430\u043c \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u043e\u0440 \u043c\u043e\u0433\u0443\u0442 \u043f\u0440\u043e\u044f\u0432\u043b\u044f\u0442\u044c \u0440\u0430\u0437\u043d\u043e\u0433\u043e \u0440\u043e\u0434\u0430 \u043e\u043f\u0442\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u0438. \u042d\u0442\u0438\u00a0 \u043e\u043f\u0442\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u0438 \u0438\u0437\u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e \u0431\u044b\u043b\u0438 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u044b \u0434\u043b\u044f \u043e\u0434\u043d\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u043e\u0433\u043e \u043a\u043e\u0434\u0430, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043e\u043d\u0438 \u043c\u043e\u0433\u0443\u0442 \u043f\u0440\u0438\u0432\u0435\u0441\u0442\u0438 \u043a \u0442\u043e\u043c\u0443, \u0447\u0442\u043e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430 \u043f\u043e\u0432\u0435\u0434\u0435\u0442 \u0441\u0435\u0431\u044f \u0441\u043e\u0432\u0441\u0435\u043c \u043d\u0435 \u0442\u0430\u043a \u043a\u0430\u043a \u0432\u044b \u0445\u043e\u0442\u0438\u0442\u0435 (\u043f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 <a href=\"https:\/\/habr.com\/ru\/company\/JetBrains-education\/blog\/523298\/\"><u>\u0442\u0443\u0442<\/u><\/a>). \u041d\u0443 \u0438 \u043e\u0442\u043b\u0438\u0447\u0438\u044f \u0432 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u044f\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u043a\u0430\u043a \u0440\u0430\u0437 \u043e\u0431\u0443\u0441\u043b\u0430\u0432\u043b\u0438\u0432\u0430\u044e\u0442\u0441\u044f \u0442\u0435\u043c, \u0447\u0442\u043e \u043f\u0440\u0438 \u0440\u0430\u0437\u043d\u044b\u0445\u00a0 \u044d\u043d\u0432\u0430\u0439\u0440\u043e\u043d\u043c\u0435\u043d\u0442\u0430\u0445 \u044d\u0442\u0438 \u043e\u043f\u0442\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u0438 \u0440\u0430\u0437\u043d\u044b\u0435. \u041c\u043e\u0434\u0435\u043b\u0438 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u044f \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u043d\u0430\u0437\u044b\u0432\u0430\u044e\u0442\u0441\u044f \u043c\u043e\u0434\u0435\u043b\u044f\u043c\u0438 \u043f\u0430\u043c\u044f\u0442\u0438 (\u0434\u0430\u043b\u0435\u0435 MM). \u0421\u0430\u043c\u0430\u044f \u043f\u0440\u043e\u0441\u0442\u0430\u044f \u0438 \u0438\u0437\u0432\u0435\u0441\u0442\u043d\u0430\u044f MM \u2014 \u044d\u0442\u043e <a href=\"https:\/\/en.wikipedia.org\/wiki\/Sequential_consistency\"><u>Sequential Consistency<\/u><\/a>.\u00a0<\/p>\n<p>\u0415\u0441\u043b\u0438 \u043c\u044b \u0445\u043e\u0440\u043e\u0448\u043e \u0438\u0437\u0443\u0447\u0438\u043c \u043a\u043e\u043d\u043a\u0440\u0435\u0442\u043d\u0443\u044e \u041c\u041c, \u0442\u043e \u0441\u043c\u043e\u0436\u0435\u043c \u043f\u043e \u0433\u0440\u0430\u0444\u0443 \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0433\u043e\u0432\u043e\u0440\u0438\u0442\u044c, \u0434\u043e\u043f\u0443\u0441\u0442\u0438\u043c \u043e\u043d \u0438\u043b\u0438 \u043d\u0435\u0442 \u043f\u0440\u0438 \u0434\u0430\u043d\u043d\u043e\u0439 \u041c\u041c. \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u041c\u041c \u0447\u0430\u0441\u0442\u043e \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u0443\u044e\u0442\u0441\u044f \u043f\u0440\u043e\u0441\u0442\u043e\u00a0 \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u0430\u043c\u0438 \u043d\u0430 \u0433\u0440\u0430\u0444\u0430\u0445.<\/p>\n<h3>\u041e \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0430\u0445 model checker<\/h3>\n<p>\u0418\u0442\u0430\u043a, \u0437\u0430\u0434\u0430\u0447\u0430 MC \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432 \u043f\u0435\u0440\u0435\u0431\u043e\u0440\u0435 \u0432\u0441\u0435\u0445 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0445 \u0433\u0440\u0430\u0444\u043e\u0432 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0445 \u0434\u0430\u043d\u043d\u043e\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435.\u00a0<\/p>\n<p>MC \u043c\u043e\u0436\u043d\u043e \u043e\u0446\u0435\u043d\u0438\u0432\u0430\u0442\u044c \u043f\u043e \u0431\u043e\u043b\u044c\u0448\u043e\u043c\u0443 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u0443 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u043e\u0432, \u0432\u043e\u0442 \u0442\u0440\u0438 \u0438\u0437 \u043d\u0438\u0445:<\/p>\n<ol>\n<li>\n<p>\u041e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u043e\u0441\u0442\u044c: \u0442\u0430\u043a \u043a\u0430\u043a MC \u0437\u0430\u043d\u0438\u043c\u0430\u0435\u0442\u0441\u044f \u043e\u0431\u0445\u043e\u0434\u043e\u043c \u0433\u0440\u0430\u0444\u043e\u0432, \u043c\u043e\u0436\u043d\u043e \u0433\u043e\u0432\u043e\u0440\u0438\u0442\u044c, \u0447\u0442\u043e \u043e\u043d \u043e\u043f\u0442\u0438\u043c\u0430\u043b\u0435\u043d \u0435\u0441\u043b\u0438 \u043e\u0431\u0445\u043e\u0434\u0438\u0442 \u043a\u0430\u0436\u0434\u044b\u0439 \u0433\u0440\u0430\u0444 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435 \u0440\u043e\u0432\u043d\u043e \u043e\u0434\u0438\u043d \u0440\u0430\u0437<\/p>\n<\/li>\n<li>\n<p>Stateless\/explicit-state: MC \u043c\u043e\u0436\u0435\u0442 \u0445\u0440\u0430\u043d\u0438\u0442\u044c \u043a\u0430\u043a\u0438\u0435-\u0442\u043e \u0434\u0430\u043d\u043d\u044b\u0435 \u043e \u0433\u0440\u0430\u0444\u0430\u0445, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u043d \u0443\u0436\u0435 \u043e\u0431\u043e\u0448\u0435\u043b. \u0415\u0441\u043b\u0438 \u043e\u043d \u0432\u043e\u043e\u0431\u0449\u0435 \u043d\u0438\u043a\u0430\u043a\u043e\u0439 \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u0438 \u043d\u0435 \u0445\u0440\u0430\u043d\u0438\u0442, \u0442\u043e \u0431\u0443\u0434\u0435\u043c \u043d\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0435\u0433\u043e Stateless.\u00a0<\/p>\n<\/li>\n<li>\n<p>\u041f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0438\u0447\u043d\u043e\u0441\u0442\u044c \u043f\u043e MM: \u0431\u0443\u0434\u0435\u043c \u0433\u043e\u0432\u043e\u0440\u0438\u0442\u044c, \u0447\u0442\u043e \u041c\u0421 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0438\u0447\u0435\u043d \u043f\u043e MM, \u0435\u0441\u043b\u0438 \u043e\u043d \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0434\u043b\u044f \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 MM. \u041c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u044d\u0442\u043e \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u0443\u0435\u0442\u0441\u044f \u0442\u0430\u043a, \u0447\u0442\u043e MC \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043d\u0430 \u0432\u0445\u043e\u0434 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442 \u043d\u0430 \u0433\u0440\u0430\u0444\u0430\u0445 \u0438\u0441\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u044f <code>cons<\/code> \u0438 \u0434\u0430\u043b\u044c\u0448\u0435 \u0438\u0441\u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0433\u0440\u0430\u0444\u044b, \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0435 \u044d\u0442\u043e\u043c\u0443 \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u0443.<\/p>\n<\/li>\n<\/ol>\n<p><a href=\"https:\/\/plv.mpi-sws.org\/genmc\/\"><u>\u0421\u0430\u043c\u044b\u0435 \u0443\u0441\u043f\u0435\u0448\u043d\u044b\u0435 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0435 MC<\/u><\/a> \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0438\u0447\u043d\u044b\u043c\u0438 \u043f\u043e \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0430\u043c\u044f\u0442\u0438, \u043e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u044b\u043c\u0438 \u0438 \u043f\u043e\u0447\u0442\u0438 Stateless. \u0422\u043e \u0435\u0441\u0442\u044c \u043e\u043d\u0438 \u043d\u0435 \u043f\u043e\u0441\u0435\u0449\u0430\u044e\u0442 \u043e\u0434\u043d\u0438 \u0438 \u0442\u0435 \u0436\u0435 \u0433\u0440\u0430\u0444\u044b \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0440\u0430\u0437, \u043e\u0434\u043d\u0430\u043a\u043e, \u0445\u0440\u0430\u043d\u044f\u0442 \u043a\u0430\u043a\u0443\u044e-\u0442\u043e \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043e \u0441\u0432\u043e\u0435\u0439 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0440\u0430\u0431\u043e\u0442\u0435, \u0447\u0442\u043e \u0432\u0435\u0434\u0435\u0442 \u043a \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u043c \u0437\u0430\u0442\u0440\u0430\u0442\u0430\u043c \u043f\u043e \u043f\u0430\u043c\u044f\u0442\u0438.\u00a0<\/p>\n<h3>\u041e TruSt<\/h3>\n<p>\u041d\u0430\u043a\u043e\u043d\u0435\u0446, \u043d\u043e\u0432\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u044b\u043b \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d \u0432 MPI-SWS, \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043f\u0435\u0440\u0432\u044b\u043c \u043e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u044b\u043c, \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0438\u0447\u043d\u044b\u043c \u043f\u043e \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0430\u043c\u044f\u0442\u0438 \u0438 \u0432 \u0442\u043e \u0436\u0435 \u0432\u0440\u0435\u043c\u044f Stateless (\u0432\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u0435 \u0447\u0435\u0433\u043e \u0438\u043c\u0435\u0435\u0442 \u043b\u0438\u043d\u0435\u0439\u043d\u044b\u0435 \u0437\u0430\u0442\u0440\u0430\u0442\u044b \u043f\u043e \u043f\u0430\u043c\u044f\u0442\u0438). \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u043e\u043d \u0438 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f TruSt (Truly Stateless).<\/p>\n<p>T\u0443\u0442, \u043e\u0434\u043d\u0430\u043a\u043e, \u0441\u0442\u043e\u0438\u0442 \u043e\u0442\u043c\u0435\u0442\u0438\u0442\u044c, \u0447\u0442\u043e \u043e\u043d \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u043d\u0435 \u0434\u043b\u044f \u0432\u0441\u0435\u0445 \u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u043f\u0430\u043c\u044f\u0442\u0438, \u0430 \u043b\u0438\u0448\u044c \u0434\u043b\u044f \u0442\u0435\u0445, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u043c \u0443\u0441\u043b\u043e\u0432\u0438\u044f\u043c. \u0421\u044e\u0434\u0430 \u043f\u043e\u0434\u0445\u043e\u0434\u044f\u0442 \u0442\u0430\u043a\u0438\u0435 \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0430\u043c\u044f\u0442\u0438, \u043a\u0430\u043a <a href=\"https:\/\/ieeexplore.ieee.org\/document\/1675439\"><u>Sequential consistency <\/u><\/a>(SC), <a href=\"https:\/\/link.springer.com\/chapter\/10.1007%2F978-3-642-03359-9_27\"><u>Total store ordering<\/u><\/a> (TSO) (\u0435\u0449\u0435 \u043f\u0440\u043e \u044d\u0442\u0443 \u043c\u043e\u0434\u0435\u043b\u044c \u043c\u043e\u0436\u043d\u043e \u043f\u043e\u0447\u0438\u0442\u0430\u0442\u044c <a href=\"https:\/\/habr.com\/ru\/company\/JetBrains-education\/blog\/523298\/\"><u>\u0442\u0443\u0442<\/u><\/a>), <a href=\"https:\/\/www.cs.utexas.edu\/users\/novak\/sparcv9.pdf\"><u>Partial store ordering<\/u><\/a> (PSO), \u0430 \u0442\u0430\u043a\u0436\u0435<a href=\"https:\/\/dl.acm.org\/doi\/10.1145\/3062341.3062352\"><u> \u0444\u0440\u0430\u0433\u043c\u0435\u043d\u0442 \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0430\u043c\u044f\u0442\u0438 \u044f\u0437\u044b\u043a\u0430 \u0421\/\u0421++ <\/u><\/a>(RC11).<\/p>\n<p>MC \u0438\u0449\u0435\u0442 \u043e\u0448\u0438\u0431\u043a\u0438 \u0432 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u043e\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435, \u043d\u043e \u043a\u0442\u043e \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u0435\u0442, \u0447\u0442\u043e \u0432 \u0441\u0430\u043c\u043e\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0435 \u041c\u0421 \u043d\u0435\u0442 \u043e\u0448\u0438\u0431\u043e\u043a? \u0412\u0435\u0434\u044c \u0435\u0441\u043b\u0438 \u043e\u043d\u0438 \u0435\u0441\u0442\u044c, model checker \u043c\u043e\u0436\u0435\u0442 \u0432\u0432\u0435\u0441\u0442\u0438 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044f \u0432 \u0437\u0430\u0431\u043b\u0443\u0436\u0434\u0435\u043d\u0438\u0435. \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u0432\u0430\u0436\u043d\u043e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u041c\u0421. \u041a\u0430\u043a \u0440\u0430\u0437 \u044d\u0442\u0438\u043c \u044f \u0438 \u0437\u0430\u043d\u0438\u043c\u0430\u043b\u0441\u044f. \u042f \u0432\u0437\u044f\u043b \u043f\u0441\u0435\u0432\u0434\u043e\u043a\u043e\u0434, \u043d\u0430 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0431\u044b\u043b \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d \u0432 \u0441\u0442\u0430\u0442\u044c\u0435, \u0437\u0430\u043a\u043e\u0434\u0438\u0440\u043e\u0432\u0430\u043b \u044d\u0442\u043e \u0432 Coq \u0438 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u043b \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u044d\u0442\u043e\u0433\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430.<\/p>\n<p>\u041a \u0441\u043e\u0436\u0430\u043b\u0435\u043d\u0438\u044e, \u0441\u0430\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0443\u0441\u0442\u0440\u043e\u0435\u043d \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u0441\u043b\u043e\u0436\u043d\u043e, \u0438 \u044f \u043d\u0435 \u0441\u043c\u043e\u0433\u0443 \u0435\u0433\u043e \u0437\u0434\u0435\u0441\u044c \u043e\u043f\u0438\u0441\u0430\u0442\u044c. \u0412\u0441\u0435 \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u043e\u0441\u0442\u0438 \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 \u0432 <a href=\"https:\/\/people.mpi-sws.org\/~viktor\/papers\/popl2022-trust.pdf\"><u>\u0441\u0442\u0430\u0442\u044c\u0435<\/u><\/a>. \u0410 \u0441\u0435\u0439\u0447\u0430\u0441 \u044f \u0440\u0430\u0441\u0441\u043a\u0430\u0436\u0443 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u043e\u0431\u0449\u0443\u044e \u0441\u0445\u0435\u043c\u0443 \u0442\u043e\u0433\u043e, \u043a\u0430\u043a \u043e\u043d \u0431\u044b\u043b \u0437\u0430\u043a\u043e\u0434\u0438\u0440\u043e\u0432\u0430\u043d \u043d\u0430 \u044f\u0437\u044b\u043a\u0435 Coq.<\/p>\n<p>\u0417\u0430\u0444\u0438\u043a\u0441\u0438\u0440\u0443\u0435\u043c \u0434\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442 \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0430\u043c\u044f\u0442\u0438 \u043d\u0430 \u0433\u0440\u0430\u0444\u0430\u0445 <code>\u0441ons<\/code>:<\/p>\n<pre><code>  procedure Verify(P) \/\/ \u0413\u043b\u0430\u0432\u043d\u0430\u044f \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0430: \u0431\u0435\u0440\u0435\u0442 \u043d\u0430 \u0432\u0445\u043e\u0434 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0443 P \u0438 \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u0435\u0442 \u0432\u0441\u043f\u043e\u043c\u043e\u0433\u0430\u0442\u0435\u043b\u044c\u043d\u0443\u044e \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 Visit    Visit(P, G0) \/\/ Visit \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u0435\u0442\u0441\u044f \u043e\u0442 \u043d\u0430\u0448\u0435\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0438 \u043f\u0443\u0441\u0442\u043e\u0433\u043e \u0433\u0440\u0430\u0444\u0430 \u0438 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u043e \u0438\u0441\u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0432\u0441\u0435 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0435 \u0433\u0440\u0430\u0444\u044b    procedure Visit(P, G) \/\/ \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u044b \u0438\u0441\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u043d\u0438\u0435 \u0433\u0440\u0430\u0444\u043e\u0432    if !cons G then return \/\/ \u0435\u0441\u043b\u0438 \u0433\u0440\u0430\u0444 \u043d\u0435 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u0435\u0442 \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u0443 \u043a\u043e\u043d\u0441\u0438\u0441\u0435\u0442\u043d\u043e\u0441\u0442\u0438 \u0442\u043e \u0432\u044b\u0445\u043e\u0434\u0438\u043c \u0438\u0437 \u0446\u0438\u043a\u043b\u0430    a := next(P, G) \/\/ \u0432\u044b\u0431\u0438\u0440\u0430\u0435\u043c \u043a\u0430\u043a\u0443\u044e \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044e \u0432 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435 \u043d\u0430\u0434\u043e \u0438\u0441\u043f\u043e\u043b\u043d\u0438\u0442\u044c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0439 \u0438 \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u043c \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u044e\u0449\u0435\u0435 \u0441\u043e\u0431\u044b\u0442\u0438\u0435 a \u0432 G    switch a do      case a = \u22a5 \/\/ \u0435\u0441\u043b\u0438 \u0432 a \u043d\u0438\u0447\u0435\u0433\u043e \u043d\u0435 \u0437\u0430\u043f\u0438\u0441\u0430\u043b\u043e\u0441\u044c, \u0437\u043d\u0430\u0447\u0438\u0442 \u043c\u044b \u0438\u0441\u043f\u043e\u043b\u043d\u0438\u043b\u0438 \u0432\u0441\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u0438        return \u201cOK\u201d     case a \u2208 error \/\/ \u0435\u0441\u043b\u0438 \u0430 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u043d\u0430\u0440\u0443\u0448\u0435\u043d\u0438\u044e assert\u2019\u0430 \u0438\u043b\u0438 \u043a\u0430\u043a\u043e\u0439-\u0442\u043e \u043e\u0448\u0438\u0431\u043a\u0435 \u0442\u043e \u0432\u0435\u0440\u043d\u0435\u043c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u043e\u0431 \u043e\u0448\u0438\u0431\u043a\u0435       exit(\u201cerror\u201d)     \u2026 \/\/ \u0432 \u0438\u043d\u044b\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445 \u043c\u044b \u0431\u0443\u0434\u0435\u043c \u0445\u0438\u0442\u0440\u043e \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u043e \u0432\u044b\u0437\u044b\u0432\u0430\u0442\u044c\u0441\u044f \u043d\u0430 \u043a\u0430\u043a\u0438\u0445-\u0442\u043e \u0434\u0440\u0443\u0433\u0438\u0445 \u0433\u0440\u0430\u0444\u0430\u0445<\/code><\/pre>\n<p>\u041f\u0440\u0438\u043c\u0435\u0440\u043d\u043e \u0442\u0430\u043a \u044d\u0442\u043e\u0442 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0438 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d. \u041f\u043e\u0441\u043c\u043e\u0442\u0440\u0438\u043c, \u043a\u0430\u043a \u0435\u0433\u043e \u043a\u043e\u0434\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0432 Coq.<\/p>\n<p>\u0411\u0443\u0434\u0435\u043c \u0433\u043e\u0432\u043e\u0440\u0438\u0442\u044c, \u0447\u0442\u043e \u0433\u0440\u0430\u0444 G1 \u0441\u0432\u044f\u0437\u0430\u043d \u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u0435\u043c \u21d2 \u0441 \u0433\u0440\u0430\u0444\u043e\u043c G2 (\u0438 \u043f\u0438\u0441\u0430\u0442\u044c G1\u00a0 \u21d2\u00a0 G2) \u0435\u0441\u043b\u0438 <code>Visit(P, G1)<\/code> \u0432\u044b\u0437\u043e\u0432\u0435\u0442\u00a0 <code>Visit(P, G2) <\/code>\u043d\u0430 \u0432\u0435\u0440\u0445\u043d\u0435\u043c \u0443\u0440\u043e\u0432\u043d\u0435 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0438. \u0414\u0430\u043b\u0435\u0435 \u0432\u0432\u0435\u0434\u0435\u043c \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u0431\u043e\u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f:<\/p>\n<ol>\n<li>\n<p>G1 \u21d2k G2 \u0431\u0443\u0434\u0435\u0442 \u0437\u043d\u0430\u0447\u0438\u0442\u044c, \u0447\u0442\u043e G1 \u21d2 ..k \u0440\u0430\u0437&#8230; \u21d2 G2<\/p>\n<\/li>\n<li>\n<p>G1 \u21d2* G2 \u0431\u0443\u0434\u0435\u0442 \u0437\u043d\u0430\u0447\u0438\u0442\u044c, \u0447\u0442\u043e \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 k \u0442\u0430\u043a\u043e\u0439, \u0447\u0442\u043e G1 \u21d2k G2<\/p>\n<\/li>\n<\/ol>\n<h3>\u041e \u0442\u043e\u043c, \u0447\u0442\u043e \u044f \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u043b \u043d\u0430 Coq<\/h3>\n<p><strong>\u041a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c<\/strong><\/p>\n<p><code>Theorem TruSt_Correct : forall G, G0 \u21d2* G -> cons G<\/code><\/p>\n<p>\u042d\u0442\u0430 \u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u0433\u043e\u0432\u043e\u0440\u0438\u0442 \u043e \u0442\u043e\u043c, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u043c\u044b \u0437\u0430 \u043a\u0430\u043a\u043e\u0435-\u0442\u043e \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0448\u0430\u0433\u043e\u0432 \u043c\u043e\u0436\u0435\u043c \u0434\u043e\u0439\u0442\u0438 \u0438\u0437 \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0433\u0440\u0430\u0444\u0430 \u0432 \u0433\u0440\u0430\u0444 G, \u0442\u043e \u0433\u0440\u0430\u0444 G \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043a\u043e\u043d\u0441\u0438\u0441\u0442\u0435\u043d\u0442\u043d\u044b\u043c. \u042d\u0442\u0430 \u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u0442\u0440\u0438\u0432\u0438\u0430\u043b\u044c\u043d\u043e, \u0442\u0430\u043a \u043a\u0430\u043a \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u044f\u0432\u043d\u043e \u043d\u0430 \u043a\u0430\u0436\u0434\u043e\u043c \u0448\u0430\u0433\u0435 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442 \u0433\u0440\u0430\u0444\u044b \u043d\u0430 \u043a\u043e\u043d\u0441\u0438\u0441\u0442\u0435\u043d\u0442\u043d\u043e\u0441\u0442\u044c.\u00a0<\/p>\n<p><strong>\u0422\u0435\u0440\u043c\u0438\u043d\u0438\u0440\u0443\u0435\u043c\u043e\u0441\u0442\u044c\u00a0<\/strong><\/p>\n<p><code>Theorem TruSt_Terminate : exists B, forall G, G0 \u21d2k G -> k &lt; B<\/code><\/p>\n<p>\u0415\u0441\u0442\u044c \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043e\u0446\u0435\u043d\u043a\u0430 \u043d\u0430 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0432\u043b\u043e\u0436\u0435\u043d\u043d\u044b\u0445 \u0432\u044b\u0437\u043e\u0432\u043e\u0432 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430. \u0422\u0443\u0442 \u043d\u0430\u0434\u043e \u043f\u043e\u044f\u0441\u043d\u0438\u0442\u044c, \u0447\u0442\u043e \u0432\u0435\u0441\u044c \u044d\u0442\u043e\u0442 \u043c\u0435\u0442\u043e\u0434 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0442\u043e\u043b\u044c\u043a\u043e \u0434\u043b\u044f \u043a\u043e\u043d\u0435\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c. \u0422\u043e \u0435\u0441\u0442\u044c \u044d\u0442\u043e \u0434\u043e\u043b\u0436\u043d\u044b \u0431\u044b\u0442\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0431\u0435\u0437 \u0431\u0435\u0441\u043a\u043e\u043d\u0435\u0447\u043d\u044b\u0445 \u0446\u0438\u043a\u043b\u043e\u0432 \u0438 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0439 (\u0435\u0441\u043b\u0438 \u0432 \u043d\u0430\u0448\u0435\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435 \u0435\u0441\u0442\u044c \u043f\u043e\u0442\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e \u0431\u0435\u0441\u043a\u043e\u043d\u0435\u0447\u043d\u044b\u0439 \u0446\u0438\u043a\u043b, \u0442\u043e \u043c\u044b \u043f\u0440\u043e\u0441\u0442\u043e \u0440\u0430\u0437\u0432\u043e\u0440\u0430\u0447\u0438\u0432\u0430\u0435\u043c \u0435\u0433\u043e \u043d\u0430 \u043d\u0430\u043f\u0435\u0440\u0435\u0434 \u0437\u0430\u0434\u0430\u043d\u043d\u0443\u044e \u0433\u043b\u0443\u0431\u0438\u043d\u0443 \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u043f\u043e \u043c\u043e\u0434\u0443\u043b\u044e \u044d\u0442\u043e\u0439 \u0433\u043b\u0443\u0431\u0438\u043d\u044b). \u0414\u0430\u043b\u0435\u0435 \u043c\u043e\u0436\u043d\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c, \u0447\u0442\u043e \u0435\u0441\u0442\u044c \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0441\u043e\u0431\u044b\u0442\u0438\u044f, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043d\u0438\u043a\u043e\u0433\u0434\u0430 \u043d\u0435 \u0443\u0434\u0430\u043b\u044f\u044e\u0442\u0441\u044f (\u0430 \u0442\u043e\u043b\u044c\u043a\u043e \u0434\u043e\u0431\u0430\u0432\u043b\u044f\u044e\u0442\u0441\u044f) \u0432 \u0445\u043e\u0434\u0435 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u044b\u0445 \u0432\u044b\u0437\u043e\u0432\u043e\u0432 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430. \u0418\u0437 \u044d\u0442\u043e\u0433\u043e \u043b\u0435\u0433\u043a\u043e \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0442\u0435\u0440\u043c\u0438\u043d\u0438\u0440\u0443\u0435\u043c\u043e\u0441\u0442\u044c.<\/p>\n<p><strong>\u041f\u043e\u043b\u043d\u043e\u0442\u0430<\/strong><\/p>\n<p><code>Theorem TruSt_Complete : forall G, cons G \/\\ p_sem G -> G0 \u21d2* G<\/code><\/p>\n<p>\u0422\u0443\u0442 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043e, \u0447\u0442\u043e \u0435\u0441\u043b\u0438<\/p>\n<ol>\n<li>\n<p><code>cons G<\/code> \u2014 \u0433\u0440\u0430\u0444 G \u043a\u043e\u043d\u0441\u0438\u0441\u0442\u0435\u043d\u0442\u0435\u043d<\/p>\n<\/li>\n<li>\n<p>p<code>_sem G<\/code> \u2014 \u0433\u0440\u0430\u0444 G \u043a\u043e\u0434\u0438\u0440\u0443\u0435\u0442 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u043d\u0430\u0448\u0435\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b,<\/p>\n<\/li>\n<\/ol>\n<p>\u0442\u043e \u043c\u044b \u044d\u0442\u043e\u0442 \u0433\u0440\u0430\u0444 \u0432\u0441\u0442\u0440\u0435\u0442\u0438\u043c \u043d\u0430 \u043a\u0430\u043a\u043e\u043c-\u0442\u043e \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u043e\u043c \u0432\u044b\u0437\u043e\u0432\u0435. \u0422\u043e \u0435\u0441\u0442\u044c \u044d\u0442\u0430 \u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u0435\u0442, \u0447\u0442\u043e \u043c\u044b \u0442\u043e\u0447\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u043c \u0432\u0441\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u0438\u0441\u0445\u043e\u0434\u044b.<\/p>\n<p>\u042d\u0442\u043e \u043e\u0434\u043d\u0430 \u0438\u0437 \u0441\u0430\u043c\u044b\u0445 \u0441\u043b\u043e\u0436\u043d\u044b\u0445 \u0442\u0435\u043e\u0440\u0435\u043c. \u0414\u043b\u044f \u0435\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u043f\u0440\u0438\u0448\u043b\u043e\u0441\u044c \u043f\u043e\u0441\u0442\u0440\u043e\u0438\u0442\u044c \u043e\u0431\u0440\u0430\u0442\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0434\u043b\u044f <code>Visit: Prev<\/code>. \u0422\u043e \u0435\u0441\u0442\u044c <code>Prev<\/code> \u043a\u0430\u0436\u0434\u043e\u043c\u0443 \u043a\u043e\u043d\u0441\u0438\u0441\u0442\u0435\u043d\u0442\u043d\u043e\u043c\u0443 \u0433\u0440\u0430\u0444\u0443 (\u043e\u0442\u043d\u043e\u0441\u0438\u0442\u0435\u043b\u044c\u043d\u043e <code>cons<\/code>) \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0435\u0433\u043e \u043d\u0435\u043f\u043e\u0441\u0440\u0435\u0434\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0433\u043e \u043f\u0440\u0435\u0434\u043a\u0430 \u043e\u0442\u043d\u043e\u0441\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u21d2 (\u0435\u0441\u043b\u0438 \u043e\u043d \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442). Prev \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442\u0441\u044f \u0437\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043d\u0430\u043c\u043d\u043e\u0433\u043e \u043f\u0440\u043e\u0449\u0435, \u0447\u0435\u043c Visit, \u0431\u043e\u043b\u0435\u0435 \u0442\u043e\u0433\u043e, \u043e\u043d \u0431\u0443\u0434\u0435\u0442 \u0434\u0435\u0442\u0435\u0440\u043c\u0438\u043d\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u043c, \u0442\u0430\u043a \u0447\u0442\u043e \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u0434\u043b\u044f \u043d\u0435\u0433\u043e \u043f\u0440\u043e\u0449\u0435. \u0414\u0430\u043b\u0435\u0435 \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u044e\u0442\u0441\u044f \u0434\u0432\u0435 \u0432\u0435\u0449\u0438:<\/p>\n<ol>\n<li>\n<p>\u0435\u0441\u043b\u0438 <code>Prev G = G\u2019<\/code>, \u0442\u043e <code>G\u2019 \u21d2 G<\/code><\/p>\n<\/li>\n<li>\n<p>\u0435\u0441\u043b\u0438 \u00a0<code>cons G<\/code> \u0438 <code>p_sem G<\/code>, \u0442\u043e \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u044f <code>Prev<\/code> \u043a <code>G<\/code> \u043c\u044b \u0432\u0441\u0435\u0433\u0434\u0430 \u043f\u0440\u0438\u0434\u0435\u043c \u043a \u043f\u0443\u0441\u0442\u043e\u043c\u0443 \u0433\u0440\u0430\u0444\u0443.<\/p>\n<\/li>\n<\/ol>\n<p>\u0418\u0437 \u044d\u0442\u043e\u0433\u043e \u043b\u0435\u0433\u043a\u043e \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0442\u0435\u043e\u0440\u0435\u043c\u0430.<\/p>\n<p><strong>\u041e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u043e\u0441\u0442\u044c<\/strong><\/p>\n<p>\u0412 Coq \u0435\u0435 \u0441\u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043d\u0435 \u043e\u0447\u0435\u043d\u044c \u043f\u0440\u043e\u0441\u0442\u043e, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043f\u043e\u043a\u0430\u0436\u0443 \u0441\u0445\u0435\u043c\u0430\u0442\u0438\u0447\u043d\u043e. \u041f\u0443\u0441\u0442\u044c<\/p>\n<ul>\n<li>\n<p><code>G0 \u21d2 G1 \u21d2 G2 \u21d2 \u2026 \u21d2 Gn<\/code> \u0435\u0441\u0442\u044c \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0448\u0430\u0433\u043e\u0432 \u0438\u0437 \u043f\u0443\u0441\u0442\u043e\u0433\u043e \u0433\u0440\u0430\u0444\u0430 \u0432 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 Gn<\/p>\n<\/li>\n<li>\n<p><code>G0 \u21d2 H1 \u21d2 H2 \u21d2 \u2026 \u21d2 Hn<\/code> \u0435\u0441\u0442\u044c \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0448\u0430\u0433\u043e\u0432 \u0438\u0437 \u043f\u0443\u0441\u0442\u043e\u0433\u043e \u0433\u0440\u0430\u0444\u0430 \u0432 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 Hn \u0438<\/p>\n<\/li>\n<li>\n<p><code>Hn = Gn<\/code>\u00a0<\/p>\n<\/li>\n<\/ul>\n<p>\u0422\u043e\u0433\u0434\u0430 \u0438 \u0432\u0441\u0435 \u043f\u0440\u043e\u043c\u0435\u0436\u0443\u0442\u043e\u0447\u043d\u044b\u0435 \u0433\u0440\u0430\u0444\u044b \u0442\u043e\u0436\u0435 \u0431\u0443\u0434\u0443\u0442 \u0440\u0430\u0432\u043d\u044b. \u0422\u043e \u0435\u0441\u0442\u044c \u043c\u044b \u043d\u0435 \u043f\u043e\u0441\u0435\u0442\u0438\u043c \u043e\u0434\u0438\u043d \u0438 \u0442\u043e\u0442 \u0436\u0435 \u0433\u0440\u0430\u0444 \u0434\u0432\u0430 \u0440\u0430\u0437\u0430.<\/p>\n<p>\u042d\u0442\u0430 \u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u0442\u043e\u0436\u0435 \u043e\u0447\u0435\u043d\u044c \u043d\u0435\u043f\u0440\u043e\u0441\u0442\u0430\u044f \u0438 \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0438\u0437 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u043e\u0431\u0440\u0430\u0442\u043d\u0430\u044f \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0430 \u043a <code>Visit<\/code> \u0434\u0435\u0442\u0435\u0440\u043c\u0438\u043d\u0438\u0440\u043e\u0432\u0430\u043d\u0430.<\/p>\n<h3>\u0418\u0442\u043e\u0433\u0438<\/h3>\n<p>\u0412 \u0438\u0442\u043e\u0433\u0435 \u044f \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u043b \u043d\u0430 Coq \u043f\u043e\u043b\u043d\u044b\u0439 \u043d\u0430\u0431\u043e\u0440 \u0442\u0435\u043e\u0440\u0435\u043c \u043f\u0440\u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u043d\u043e\u0433\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430. \u0412 \u0445\u043e\u0434\u0435 \u044d\u0442\u043e\u0439 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0431\u044b\u043b\u043e:<\/p>\n<ol>\n<li>\n<p>\u041d\u0430\u0439\u0434\u0435\u043d\u0430 \u043a\u0443\u0447\u0430 \u043e\u0448\u0438\u0431\u043e\u043a \u0438 \u043d\u0435\u0442\u043e\u0447\u043d\u043e\u0441\u0442\u0435\u0439 \u0432 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430\u0445 \u043d\u0430 \u0431\u0443\u043c\u0430\u0436\u043a\u0435. \u041d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043b\u0435\u043c\u043c\u044b \u043d\u0435 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u043b\u0438\u0441\u044c \u0432 \u0442\u043e\u043c \u0432\u0438\u0434\u0435, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u043e\u043d\u0438 \u0431\u044b\u043b\u0438 \u0441\u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u044b, \u0438 \u043f\u0440\u0438\u0448\u043b\u043e\u0441\u044c \u043f\u0440\u0438\u0434\u0443\u043c\u044b\u0432\u0430\u0442\u044c \u043d\u043e\u0432\u044b\u0435 \u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u043a\u0438.\u00a0<\/p>\n<\/li>\n<li>\n<p>\u041d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0442\u0435\u043e\u0440\u0435\u043c\u044b (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u043e\u0431 \u043e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u043e\u0441\u0442\u0438) \u0431\u044b\u043b\u0438 \u043f\u0435\u0440\u0435\u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u044b, \u0447\u0442\u043e\u0431 \u0442\u043e\u0447\u043d\u0435\u0435 \u0443\u0445\u0432\u0430\u0442\u0438\u0442\u044c \u0441\u0443\u0442\u044c \u0432\u0435\u0449\u0438, \u043a\u043e\u0442\u043e\u0440\u0443\u044e \u043c\u044b \u0445\u043e\u0442\u0438\u043c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c.<\/p>\n<\/li>\n<li>\n<p>\u0422\u0430\u043a\u0436\u0435 \u0432\u00a0 \u0445\u043e\u0434\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u044f \u0437\u0430\u043c\u0435\u0442\u0438\u043b, \u0447\u0442\u043e \u043e\u0434\u043d\u043e \u043c\u0435\u0441\u0442\u043e \u0432 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0435 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0438\u0437\u0431\u044b\u0442\u043e\u0447\u043d\u044b\u043c, \u0438 \u0435\u0433\u043e \u0443\u0431\u0440\u0430\u043b\u0438. \u0415\u0441\u043b\u0438 \u0432\u043a\u0440\u0430\u0442\u0446\u0435, \u0442\u043e \u0432 \u044d\u0442\u043e\u043c \u043c\u0435\u0441\u0442\u0435 \u0434\u0435\u043b\u0430\u043b\u0430\u0441\u044c \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0441\u043b\u0435\u0434\u043e\u0432\u0430\u043b\u0430 \u0438\u0437 \u0434\u0440\u0443\u0433\u0438\u0445 \u043f\u0440\u043e\u0432\u0435\u0440\u043e\u043a. \u0422\u0430\u043a \u043a\u0430\u043a \u043d\u0430 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u044d\u0442\u043e \u043d\u0435 \u0432\u043b\u0438\u044f\u043b\u043e, \u0442\u043e \u043f\u043e\u043d\u044f\u0442\u044c, \u0447\u0442\u043e \u043e\u043d\u043e \u043b\u0438\u0448\u043d\u0435\u0435, \u0431\u044b\u043b\u043e \u043d\u0435\u043f\u0440\u043e\u0441\u0442\u043e. \u042f \u0437\u0430\u043c\u0435\u0442\u0438\u043b, \u0447\u0442\u043e \u0432 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430\u0445 \u043e\u043d\u043e \u043d\u0435 \u0438\u0433\u0440\u0430\u0435\u0442 \u0440\u043e\u043b\u0438, \u0438 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u043b \u0435\u0433\u043e \u0443\u0431\u0440\u0430\u0442\u044c.<\/p>\n<\/li>\n<\/ol>\n<h2>\u0417\u0430\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435<\/h2>\n<p>\u0412 \u044d\u0442\u043e\u043c \u043f\u0440\u043e\u0435\u043a\u0442\u0435 \u043c\u043d\u0435 \u043f\u0440\u0438\u0448\u043b\u043e\u0441\u044c \u0432\u043e \u043c\u043d\u043e\u0433\u043e\u043c \u0432\u044b\u0439\u0442\u0438 \u0438\u0437 \u0441\u0432\u043e\u0435\u0439 \u0437\u043e\u043d\u044b \u043a\u043e\u043c\u0444\u043e\u0440\u0442\u0430: \u044f \u043f\u0438\u0441\u0430\u043b \u0435\u0433\u043e \u043d\u0430 \u043d\u043e\u0432\u043e\u043c \u0434\u043b\u044f \u0441\u0435\u0431\u044f \u0434\u0438\u0430\u043b\u0435\u043a\u0442\u0435 \u044f\u0437\u044b\u043a\u0430 Coq, \u043e\u0431\u0449\u0430\u043b\u0441\u044f \u0441 \u043b\u044e\u0434\u044c\u043c\u0438 \u043d\u0430 \u0430\u043d\u0433\u043b\u0438\u0439\u0441\u043a\u043e\u043c, \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043b\u0441\u044f GitLab\u2019\u043e\u043c \u0438 \u0442.\u0434&#8230;\u00a0 \u042d\u0442\u043e \u043e\u0434\u043d\u043e\u0437\u043d\u0430\u0447\u043d\u043e \u0446\u0435\u043d\u043d\u044b\u0439 \u043e\u043f\u044b\u0442, \u043d\u043e \u0441\u0430\u043c\u043e\u0435 \u0433\u043b\u0430\u0432\u043d\u043e\u0435, \u0447\u0442\u043e \u043c\u043d\u0435 \u0443\u0434\u0430\u043b\u043e\u0441\u044c \u043f\u043e\u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c \u0441 \u043c\u0435\u0433\u0430 \u043a\u0440\u0443\u0442\u044b\u043c\u0438 \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u0438\u0441\u0442\u0430\u043c\u0438 \u0432 \u043e\u0431\u043b\u0430\u0441\u0442\u0438 Weak Memory. \u041d\u0430\u0434\u0435\u044e\u0441\u044c, \u0447\u0442\u043e \u044f \u0441\u043c\u043e\u0433\u0443 \u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0438\u0442\u044c \u0441\u043e\u0442\u0440\u0443\u0434\u043d\u0438\u0447\u0430\u0442\u044c \u0441 \u043d\u0438\u043c\u0438 \u0432 \u0431\u0443\u0434\u0443\u0449\u0435\u043c. \u042d\u0442\u043e \u0431\u044b\u043b\u0430 \u043e\u0447\u0435\u043d\u044c \u043a\u0440\u0443\u0442\u0430\u044f \u0441\u0442\u0430\u0436\u0438\u0440\u043e\u0432\u043a\u0430!<\/p>\n<p>\u041c\u043e\u0439 \u043a\u043e\u0434 \u043d\u0430 <a href=\"https:\/\/github.com\/volodeyka\/trust-coq\"><u>GitHub<\/u><\/a><\/p>\n<\/div>\n<\/div>\n<\/div>\n<p><!----><!----><\/div>\n<p><!----><!----><br \/> \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"https:\/\/habr.com\/ru\/articles\/589343\/\"> https:\/\/habr.com\/ru\/articles\/589343\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<div><!--[--><!--]--><\/div>\n<div id=\"post-content-body\">\n<div>\n<div class=\"article-formatted-body article-formatted-body article-formatted-body_version-2\">\n<div xmlns=\"http:\/\/www.w3.org\/1999\/xhtml\">\n<p>\u041d\u0430\u0434\u043e\u0435\u043b\u0438 \u043d\u0435\u0441\u0442\u0430\u0431\u0438\u043b\u044c\u043d\u044b\u0435 \u0431\u0430\u0433\u0438 \u0432 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u043e\u043c \u043a\u043e\u0434\u0435? \u041f\u043e\u043f\u0440\u043e\u0431\u0443\u0439 \u0432\u043e\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c\u0441\u044f \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u0430\u043c\u0438! \u0412\u0435\u0434\u044c \u0431\u043e\u043b\u044c\u0448\u0435 \u043d\u0435 \u043d\u0430\u0434\u043e \u0431\u043e\u044f\u0442\u044c\u0441\u044f \u043d\u0435\u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0445 \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u043e\u0432,\u00a0 \u0440\u0430\u0431\u043e\u0442\u0430\u044e\u0449\u0438\u0445 \u043b\u0438\u0431\u043e \u0437\u0430 \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e\u0435 \u0432\u0440\u0435\u043c\u044f, \u043b\u0438\u0431\u043e \u043d\u0435\u043e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u043e. \u0412\u0441\u0435 \u044d\u0442\u043e \u0432 \u043f\u0440\u043e\u0448\u043b\u043e\u043c: \u0432 <a href=\"https:\/\/www.mpi-sws.org\/\"><u>Max Planck Institute for Software Systems<\/u><\/a> \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043b\u0438 \u043d\u043e\u0432\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u043e\u0434 \u043d\u0430\u0437\u0432\u0430\u043d\u0438\u0435\u043c TruSt, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0440\u0435\u0448\u0430\u0435\u0442 \u044d\u0442\u0438 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0438, \u043a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d \u043d\u0430 Coq.<\/p>\n<p>\u041c\u0435\u043d\u044f \u0437\u043e\u0432\u0443\u0442 \u0412\u043b\u0430\u0434\u0438\u043c\u0438\u0440 \u0413\u043b\u0430\u0434\u0448\u0442\u0435\u0439\u043d. \u042d\u0442\u0438\u043c \u043b\u0435\u0442\u043e\u043c \u044f \u043f\u0440\u043e\u0445\u043e\u0434\u0438\u043b \u0441\u0442\u0430\u0436\u0438\u0440\u043e\u0432\u043a\u0443 \u0432 MPI-SWS \u0432 \u0433\u0440\u0443\u043f\u043f\u0435, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u0440\u0438\u0434\u0443\u043c\u0430\u043b\u0430 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043d\u043e\u0432\u043e\u0433\u043e \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u0430 \u0434\u043b\u044f \u043f\u043e\u0438\u0441\u043a\u0430 \u0431\u0430\u0433\u043e\u0432 \u0432 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430\u0445. \u042d\u0442\u043e\u0442 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043e\u043f\u0442\u0438\u043c\u0430\u043b\u044c\u043d\u044b\u043c \u0438 truly stateless (\u0432\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u0435 \u0447\u0435\u0433\u043e \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0441 \u043b\u0438\u043d\u0435\u0439\u043d\u044b\u043c\u0438 \u0437\u0430\u0442\u0440\u0430\u0442\u0430\u043c\u0438 \u043f\u043e \u043f\u0430\u043c\u044f\u0442\u0438). \u0412 \u044d\u0442\u043e\u043c \u043f\u043e\u0441\u0442\u0435 \u044f \u0440\u0430\u0441\u0441\u043a\u0430\u0436\u0443, \u043a\u0430\u043a \u0440\u0430\u0431\u043e\u0442\u0430\u044e\u0442 \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u044b, \u0432 \u043a\u0430\u043a\u0438\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445 \u0438\u0445 \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c, \u0438 \u0447\u0442\u043e \u0437\u0430 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0440\u0438\u0434\u0443\u043c\u0430\u043b\u0438 \u043c\u043e\u0438 \u043a\u043e\u043b\u043b\u0435\u0433\u0438. \u0410 \u0435\u0449\u0435 \u043a\u0430\u043a \u044f \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u043b \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0435\u0433\u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u043d\u0430 Coq.\u00a0<\/p>\n<figure class=\"full-width\"><figcaption><\/figcaption><\/figure>\n<h3>\u041e \u0441\u0435\u0431\u0435\u00a0<\/h3>\n<p>\u042f \u0443\u0447\u0443\u0441\u044c \u043d\u0430 4-\u043e\u043c \u043a\u0443\u0440\u0441\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u00ab\u041c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0430, \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u044b \u0438 \u0430\u043d\u0430\u043b\u0438\u0437 \u0434\u0430\u043d\u043d\u044b\u0445\u00bb \u0444\u0430\u043a\u0443\u043b\u044c\u0442\u0435\u0442\u0430 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0438 \u0438 \u043a\u043e\u043c\u043f\u044c\u044e\u0442\u0435\u0440\u043d\u044b\u0445 \u043d\u0430\u0443\u043a \u0421\u041f\u0431\u0413\u0423, \u0430 \u0442\u0430\u043a\u0436\u0435 \u0440\u0430\u0431\u043e\u0442\u0430\u044e \u0432 <a href=\"https:\/\/old.research.jetbrains.org\/ru\/groups\/plt_lab\"><u>\u041b\u0430\u0431\u043e\u0440\u0430\u0442\u043e\u0440\u0438\u0438 \u044f\u0437\u044b\u043a\u043e\u0432\u044b\u0445 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u0432<\/u><\/a> JetBrains Research. \u042f \u0431\u043e\u043b\u044c\u0448\u0435 \u0434\u0432\u0443\u0445 \u043b\u0435\u0442 \u0438\u0437\u0443\u0447\u0430\u044e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0443\u044e \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u0438 \u0432 \u043e\u0441\u043d\u043e\u0432\u043d\u043e\u043c \u043f\u0438\u0448\u0443 \u043d\u0430 \u044f\u0437\u044b\u043a\u0435 Coq.<\/p>\n<h3>\u041e \u0441\u0442\u0430\u0436\u0438\u0440\u043e\u0432\u043a\u0435<\/h3>\n<p>\u042d\u0442\u0438\u043c \u043b\u0435\u0442\u043e\u043c \u043c\u043d\u0435 \u043f\u043e\u0441\u0447\u0430\u0441\u0442\u043b\u0438\u0432\u0438\u043b\u043e\u0441\u044c \u043f\u0440\u043e\u0439\u0442\u0438 \u0441\u0442\u0430\u0436\u0438\u0440\u043e\u0432\u043a\u0443 \u0432 <a href=\"https:\/\/www.mpi-sws.org\/\"><u>Max Planck Institute for Software Systems<\/u><\/a>. \u041f\u043e\u043f\u0430\u043b \u044f \u0442\u0443\u0434\u0430 \u043d\u0435\u0441\u043b\u0443\u0447\u0430\u0439\u043d\u043e. \u0414\u0435\u043b\u043e \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u041b\u0430\u0431\u043e\u0440\u0430\u0442\u043e\u0440\u0438\u044f \u044f\u0437\u044b\u043a\u043e\u0432\u044b\u0445 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u0432 JBR \u0442\u0435\u0441\u043d\u043e \u0441\u043e\u0442\u0440\u0443\u0434\u043d\u0438\u0447\u0430\u0435\u0442 \u0441 \u044d\u0442\u0438\u043c \u0438\u043d\u0441\u0442\u0438\u0442\u0443\u0442\u043e\u043c. \u0412 \u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, \u0440\u0443\u043a\u043e\u0432\u043e\u0434\u0438\u0442\u0435\u043b\u044c \u043c\u043e\u0435\u0439 \u0433\u0440\u0443\u043f\u043f\u044b <a href=\"https:\/\/podkopaev.net\"><u>\u0410\u043d\u0442\u043e\u043d \u041f\u043e\u0434\u043a\u043e\u043f\u0430\u0435\u0432<\/u><\/a> \u0431\u044b\u043b \u043f\u043e\u0441\u0442\u0434\u043e\u043a\u043e\u043c \u0443 \u043f\u0440\u043e\u0444\u0435\u0441\u0441\u043e\u0440\u0430 MPI <a href=\"https:\/\/people.mpi-sws.org\/~viktor\/\"><u>\u0412\u0438\u043a\u0442\u043e\u0440\u0430 \u0412\u0430\u0444\u0435\u044f\u0434\u0438\u0441\u0430<\/u><\/a>. \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u0441 \u0440\u0435\u043a\u043e\u043c\u0435\u043d\u0434\u0430\u0446\u0438\u0435\u0439 \u043e\u0442 \u0410\u043d\u0442\u043e\u043d\u0430 \u043d\u0430 \u043c\u0435\u043d\u044f \u0431\u044b\u0441\u0442\u0440\u043e \u043e\u0431\u0440\u0430\u0442\u0438\u043b\u0438 \u0432\u043d\u0438\u043c\u0430\u043d\u0438\u0435 \u0438 \u0443\u0441\u0442\u0440\u043e\u0438\u043b\u0438 \u0441\u043e\u0431\u0435\u0441\u0435\u0434\u043e\u0432\u0430\u043d\u0438\u0435 \u0441 \u0412\u0438\u043a\u0442\u043e\u0440\u043e\u043c. \u0412 \u0438\u0442\u043e\u0433\u0435 \u043c\u0435\u043d\u044f \u0437\u0430\u0447\u0438\u0441\u043b\u0438\u043b\u0438 \u0441\u0442\u0430\u0436\u0435\u0440\u043e\u043c \u043d\u0430 \u0434\u0432\u0430 \u043c\u0435\u0441\u044f\u0446\u0430 \u2014 \u0441 \u0438\u044e\u043b\u044f \u043f\u043e \u0430\u0432\u0433\u0443\u0441\u0442 2021 \u0433\u043e\u0434\u0430. \u0421\u0442\u0430\u0436\u0438\u0440\u043e\u0432\u043a\u0430 \u043f\u0440\u043e\u0445\u043e\u0434\u0438\u043b\u0430 \u0434\u0438\u0441\u0442\u0430\u043d\u0446\u0438\u043e\u043d\u043d\u043e.<\/p>\n<h3>\u041e \u043f\u0440\u043e\u0435\u043a\u0442\u0435, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u044f \u0440\u0430\u0431\u043e\u0442\u0430\u043b<\/h3>\n<p>\u0412 \u043d\u0430\u0447\u0430\u043b\u0435 \u043b\u0435\u0442\u0430 \u043a\u043e\u043c\u0430\u043d\u0434\u0430 \u0432 MPI-SWS, \u043a \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u044f \u043f\u0440\u0438\u0441\u043e\u0435\u0434\u0438\u043d\u0438\u043b\u0441\u044f, \u0433\u043e\u0442\u043e\u0432\u0438\u043b\u0430\u0441\u044c \u043a \u043f\u043e\u0434\u0430\u0447\u0435 \u0441\u0442\u0430\u0442\u044c\u0438 \u043d\u0430 \u043a\u043e\u043d\u0444\u0435\u0440\u0435\u043d\u0446\u0438\u044e <a href=\"https:\/\/popl22.sigplan.org\/details\/POPL-2022-popl-research-papers\/49\/Truly-Stateless-Optimal-Dynamic-Partial-Order-Reduction\"><u>POPL<\/u><\/a>. \u0415\u0441\u043b\u0438 \u0432\u043a\u0440\u0430\u0442\u0446\u0435, \u043e\u043d\u0438 \u043f\u0440\u0438\u0434\u0443\u043c\u0430\u043b\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043d\u043e\u0432\u043e\u0433\u043e \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u0430 (\u0434\u0430\u043b\u0435\u0435 \u041c\u0421) \u0434\u043b\u044f \u043f\u043e\u0438\u0441\u043a\u0430 \u0431\u0430\u0433\u043e\u0432 \u0432 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430\u0445 \u0438 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u043b\u0438 \u043c\u043d\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0435\u0433\u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u043d\u0430 Coq. \u042d\u0442\u043e\u0439 \u0437\u0430\u0434\u0430\u0447\u0435\u0439 \u044f \u0438 \u0437\u0430\u043d\u0438\u043c\u0430\u043b\u0441\u044f.<\/p>\n<p>\u041d\u043e \u0434\u0430\u0432\u0430\u0439\u0442\u0435 \u043e\u0431\u043e \u0432\u0441\u0435\u043c \u043f\u043e \u043f\u043e\u0440\u044f\u0434\u043a\u0443. \u041d\u0430\u0447\u043d\u0435\u043c \u0441 Coq.<\/p>\n<h3>O Coq<\/h3>\n<p>Coq \u2014 \u044d\u0442\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u0439 \u044f\u0437\u044b\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441 \u043e\u0447\u0435\u043d\u044c \u043c\u043e\u0449\u043d\u043e\u0439 \u0441\u0438\u0441\u0442\u0435\u043c\u043e\u0439 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432. \u0421 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043d\u0435\u0435 \u043f\u043e <a href=\"https:\/\/en.wikipedia.org\/wiki\/Curry%E2%80%93Howard_correspondence\"><u>\u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u044e \u041a\u0430\u0440\u0440\u0438-\u0413\u043e\u0432\u0430\u0440\u0434\u0430<\/u><\/a> \u0432 Coq \u0443\u0434\u0430\u0435\u0442\u0441\u044f \u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0438 \u043d\u0430 \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0442\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u043d \u0441\u043c\u043e\u0436\u0435\u0442 \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c. \u041f\u0440\u0438\u043c\u0435\u0440\u044b \u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u043e\u043a \u0442\u0435\u043e\u0440\u0435\u043c \u0432 Coq \u0443 \u043d\u0430\u0441 \u0435\u0449\u0435 \u0431\u0443\u0434\u0443\u0442, \u0430 \u043f\u043e\u043a\u0430, \u0447\u0442\u043e\u0431\u044b \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0442\u044c \u043e \u0447\u0435\u043c \u0440\u0435\u0447\u044c, \u043c\u043e\u0436\u043d\u043e \u043f\u043e\u0447\u0438\u0442\u0430\u0442\u044c \u043d\u0430\u0447\u0430\u043b\u043e <a href=\"https:\/\/habr.com\/ru\/post\/182442\/\"><u>\u043c\u044f\u0433\u043a\u043e\u0433\u043e \u0432\u0432\u0435\u0434\u0435\u043d\u0438\u044f<\/u><\/a>. \u0413\u043b\u0430\u0432\u043d\u043e\u0435, \u0447\u0442\u043e \u0442\u0443\u0442 \u043d\u0430\u0434\u043e \u043f\u043e\u043d\u044f\u0442\u044c \u2014 \u043d\u0430 \u044d\u0442\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u0442\u0435\u043e\u0440\u0435\u043c\u044b, \u0438 \u043e\u043d \u0435\u0433\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442. \u0421\u0440\u0435\u0434\u0438 CS \u0441\u043e\u043e\u0431\u0449\u0435\u0441\u0442\u0432\u0430 \u0441\u0447\u0438\u0442\u0430\u0435\u0442\u0441\u044f, \u0447\u0442\u043e \u0442\u0435\u043e\u0440\u0435\u043c\u044b, \u043f\u0440\u043e\u0432\u0435\u0440\u0435\u043d\u043d\u044b\u0435 \u043d\u0430 Coq, \u043d\u0435 \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u0442 \u043e\u0448\u0438\u0431\u043e\u043a \u0432 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430\u0445.\u00a0<\/p>\n<h3>\u041e \u0431\u0430\u0433\u0430\u0445 \u0432 \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u043e\u043c \u043a\u043e\u0434\u0435\u00a0<\/h3>\n<p>\u0414\u0443\u043c\u0430\u044e \u0445\u0430\u0431\u0440\u043e\u0436\u0438\u0442\u0435\u043b\u0438 \u0437\u043d\u0430\u044e\u0442, \u0447\u0442\u043e \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u2014 \u044d\u0442\u043e \u0448\u0442\u0443\u043a\u0430 \u0441\u043b\u043e\u0436\u043d\u0430\u044f. \u0418\u043d\u043e\u0433\u0434\u0430 \u0432 \u043d\u0438\u0445 \u043f\u043e\u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u0431\u0430\u0433\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u0447\u0435\u043d\u044c \u0442\u044f\u0436\u0435\u043b\u043e \u043e\u0442\u043b\u043e\u0432\u0438\u0442\u044c \u0442\u0435\u0441\u0442\u0430\u043c\u0438. \u0422\u0430\u043a\u0438\u0435 \u0431\u0430\u0433\u0438 \u043c\u043e\u0433\u0443\u0442 \u043f\u043e\u044f\u0432\u043b\u044f\u0442\u044c\u0441\u044f \u043f\u0430\u0440\u0443 \u0440\u0430\u0437 \u043d\u0430 \u0442\u044b\u0441\u044f\u0447\u0443 \u0437\u0430\u043f\u0443\u0441\u043a\u043e\u0432 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u043e\u0434\u043d\u0430\u043a\u043e, \u0435\u0441\u043b\u0438 \u0435\u0439 \u0435\u0436\u0435\u0434\u043d\u0435\u0432\u043d\u043e \u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u043f\u043e\u0440\u044f\u0434\u043a\u0430 \u0434\u0435\u0441\u044f\u0442\u0438 \u0442\u044b\u0441\u044f\u0447 \u0447\u0435\u043b\u043e\u0432\u0435\u043a, \u0442\u043e \u0445\u043e\u0447\u0435\u0442\u0441\u044f \u043a\u0430\u043a-\u0442\u043e \u0431\u0430\u0433 \u043e\u0442\u043b\u043e\u0432\u0438\u0442\u044c \u0438 \u0438\u0441\u043f\u0440\u0430\u0432\u0438\u0442\u044c. \u041e\u0434\u043d\u0438\u043c \u0438\u0437 \u0440\u0435\u0448\u0435\u043d\u0438\u0439 \u043a\u0430\u043a \u0440\u0430\u0437 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f MC.<\/p>\n<p>\u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u0440\u0430\u0437\u0431\u0435\u0440\u0435\u043c \u043f\u0440\u0438\u043c\u0435\u0440 \u0442\u0430\u043a\u043e\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b. \u041f\u0440\u0438\u043c\u0435\u0440 \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u043e\u0431\u044a\u0435\u043c\u043d\u044b\u0439, \u043d\u043e \u043e\u043d \u043f\u043e\u043c\u043e\u0436\u0435\u0442 \u043f\u043e\u043d\u044f\u0442\u044c, \u0432 \u043a\u0430\u043a\u0438\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445 \u0440\u0430\u0437\u0443\u043c\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u043c\u043e\u0434\u0435\u043b-\u0447\u0435\u043a\u0435\u0440\u044b. \u0415\u0441\u043b\u0438 \u0445\u043e\u0442\u0438\u0442\u0435 \u043f\u0440\u043e\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u043f\u0440\u0438\u043c\u0435\u0440, \u0436\u043c\u0438\u0442\u0435 <a href=\"#1\">\u0441\u044e\u0434\u0430<\/a>.<\/p>\n<p>\u041f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u044c\u0442\u0435 \u0441\u0435\u0431\u0435 \u043b\u044e\u0431\u0438\u043c\u044b\u0439 \u0431\u0430\u043d\u043a. \u0410 \u0442\u0435\u043f\u0435\u0440\u044c \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u044c\u0442\u0435, \u0447\u0442\u043e \u0432\u0430\u0441 \u043d\u0430\u0437\u043d\u0430\u0447\u0438\u043b\u0438 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0441\u0442\u043e\u043c \u0432 \u044d\u0442\u043e\u043c \u0431\u0430\u043d\u043a\u0435 \u0438 \u043f\u043e\u043f\u0440\u043e\u0441\u0438\u043b\u0438 \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043a\u043e\u0434 \u0434\u043b\u044f \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u044f \u043e\u0447\u0435\u0440\u0435\u0434\u0435\u0439. \u0427\u0435\u043b\u043e\u0432\u0435\u043a \u043f\u0440\u0438\u0445\u043e\u0434\u0438\u0442 \u0432 \u0431\u0430\u043d\u043a, \u0431\u0435\u0440\u0435\u0442 \u043d\u043e\u043c\u0435\u0440\u043e\u043a \u0438 \u0436\u0434\u0435\u0442 \u0441\u0432\u043e\u0435\u0439 \u043e\u0447\u0435\u0440\u0435\u0434\u0438.<\/p>\n<p>\u0423\u0441\u043b\u043e\u0432\u043d\u043e \u0432\u0430\u0448\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430 \u0434\u043e\u043b\u0436\u043d\u0430 \u0443\u043c\u0435\u0442\u044c:<\/p>\n<ol>\n<li>\n<p>\u0425\u0440\u0430\u043d\u0438\u0442\u044c \u043d\u043e\u043c\u0435\u0440 \u0431\u0438\u043b\u0435\u0442\u0438\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u0434\u0430\u043d \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u043c\u0443 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0443;<\/p>\n<\/li>\n<li>\n<p>\u0425\u0440\u0430\u043d\u0438\u0442\u044c \u043d\u043e\u043c\u0435\u0440 \u0431\u0438\u043b\u0435\u0442\u0430 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0441\u0435\u0439\u0447\u0430\u0441 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u044e\u0442;<\/p>\n<\/li>\n<li>\n<p>\u0412\u044b\u0434\u0430\u0432\u0430\u0442\u044c \u043d\u043e\u0432\u044b\u0435 \u0431\u0438\u043b\u0435\u0442\u044b;<\/p>\n<\/li>\n<li>\n<p>\u041c\u0435\u043d\u044f\u0442\u044c \u043d\u043e\u043c\u0435\u0440 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u044e\u0449\u0435\u0433\u043e\u0441\u044f \u0431\u0438\u043b\u0435\u0442\u0430.<\/p>\n<\/li>\n<\/ol>\n<p>\u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u043f\u043e\u043f\u0440\u043e\u0431\u0443\u0435\u043c \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u0442\u0430\u043a\u043e\u0435 \u043d\u0430 C, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u043e\u0441\u0442\u044c. \u0421\u043d\u0430\u0447\u0430\u043b\u0430 \u0437\u0430\u0432\u0435\u0434\u0435\u043c \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u0443, \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u044e\u0449\u0443\u044e \u043f\u0430\u043c\u044f\u0442\u044c \u043d\u0430\u0448\u0435\u0433\u043e \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0430 \u043f\u043e \u0432\u044b\u0434\u0430\u0447\u0435 \u0431\u0438\u043b\u0435\u0442\u043e\u0432:<\/p>\n<pre><code class=\"cpp\">struct ticketlock_s { atomic_int next; \/\/ \u043d\u043e\u043c\u0435\u0440 \u0431\u0438\u043b\u0435\u0442\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u0434\u0430\u043d \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u043c\u0443 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0443 atomic_int owner; \/\/ \u043d\u043e\u043c\u0435\u0440 \u0431\u0438\u043b\u0435\u0442\u0430 \u0443 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430, \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0441\u0435\u0439\u0447\u0430\u0441 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u044e\u0442  };<\/code><\/pre>\n<p>\u0422\u0430\u043a \u043a\u0430\u043a \u043c\u044b \u0431\u0443\u0434\u0435\u043c \u043f\u0438\u0441\u0430\u0442\u044c \u043c\u043d\u043e\u0433\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0439 \u043a\u043e\u0434, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u043f\u043e\u043b\u044f \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u044b \u0431\u0443\u0434\u0443\u0442 \u0448\u0430\u0440\u0438\u0442\u044c\u0441\u044f \u043c\u0435\u0436\u0434\u0443 \u043f\u043e\u0442\u043e\u043a\u0430\u043c\u0438, \u043d\u0430\u043c \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u0438\u0445 \u043d\u0435 \u043f\u0440\u043e\u0441\u0442\u043e int, a <a href=\"https:\/\/en.cppreference.com\/w\/c\/language\/atomic\"><u>atomic_int<\/u><\/a>.\u00a0<\/p>\n<p>\u0422\u0435\u043f\u0435\u0440\u044c \u0434\u0430\u0432\u0430\u0439\u0442\u0435 \u043e\u043f\u0438\u0448\u0435\u043c \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 \u0432\u044b\u0434\u0430\u0447\u0438 \u0431\u0438\u043b\u0435\u0442\u0430 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0443 \u0441 \u0435\u0433\u043e \u043f\u043e\u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0436\u0438\u0434\u0430\u043d\u0438\u0435\u043c \u0441\u0432\u043e\u0435\u0439 \u043e\u0447\u0435\u0440\u0435\u0434\u0438:<\/p>\n<pre><code class=\"cpp\">static inline void ticketlock_lock(struct ticketlock_s *l) {     int ticket = atomic_load(&amp;l->next); \/\/ \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u043d\u043e\u043c\u0435\u0440 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u0431\u0438\u043b\u0435\u0442\u0430     atomic_store(&amp;l->next, ticket + 1); \/\/ \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u0432\u0430\u0435\u043c \u043d\u043e\u043c\u0435\u0440 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u0431\u0438\u043b\u0435\u0442\u0430 \u043d\u0430 1     while (atomic_load(&amp;l->owner) != ticket) { \/\/ \u0447\u0435\u043b\u043e\u0432\u0435\u043a \u0436\u0434\u0435\u0442 \u0441\u0432\u043e\u0435\u0439 \u043e\u0447\u0435\u0440\u0435\u0434\u0438     } }<\/code><\/pre>\n<p>\u0422\u0435\u043f\u0435\u0440\u044c \u043c\u043e\u0436\u043d\u043e \u043e\u043f\u0438\u0441\u0430\u0442\u044c \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 \u043f\u0435\u0440\u0435\u0445\u043e\u0434\u0430 \u043e\u0447\u0435\u0440\u0435\u0434\u0438 \u043e\u0442 \u043e\u0434\u043d\u043e\u0433\u043e \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430 \u043a \u0434\u0440\u0443\u0433\u043e\u043c\u0443:<\/p>\n<pre><code class=\"cpp\">static inline void ticketlock_unlock(struct ticketlock_s *l) {     int owner = atomic_load(&amp;l->owner); \/\/ \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c \u043d\u043e\u043c\u0435\u0440 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0435\u043c\u043e\u0433\u043e \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430     atomic_store(&amp;l->owner, owner + 1); \/\/ \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u0432\u0430\u0435\u043c \u043d\u043e\u043c\u0435\u0440 }<\/code><\/pre>\n<p>\u0414\u043b\u044f \u043f\u0440\u043e\u0441\u0442\u043e\u0442\u044b \u0431\u0443\u0434\u0435\u043c \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u0435 \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430 \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043e\u043d \u043a\u043b\u0430\u0434\u0435\u0442 \u043e\u0434\u043d\u0443 \u0434\u0435\u043d\u0435\u0436\u043a\u0443 \u043d\u0430 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0441\u0447\u0435\u0442 x, \u0430 \u043f\u043e\u0442\u043e\u043c \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430, \u0447\u0442\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435\u00a0 x \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u043b\u043e\u0441\u044c \u043d\u0430 \u043e\u0434\u0438\u043d:<\/p>\n<pre><code class=\"cpp\">int thread(void* unused) {      ticketlock_lock(&amp;lock); \/\/ \u0447\u0435\u043b\u043e\u0432\u0435\u043a \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u043d\u043e\u043c\u0435\u0440\u043e\u043a \u0438 \u0436\u0434\u0435\u0442      int y = x++; \/\/ \u0441\u043e\u0445\u0440\u0430\u043d\u044f\u0435\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 x \u0432 y \u0438 \u043a\u043b\u0430\u0434\u0435\u043c 1 \u0434\u0435\u043d\u0435\u0433 \u043d\u0430 x      assert(x == y + 1); \/\/ \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430, \u0447\u0442\u043e \u043d\u0430 x \u0431\u044b\u043b\u043e \u043f\u043e\u043b\u043e\u0436\u0435\u043d\u043e 1 \u0434\u0435\u043d\u0435\u0433      ticketlock_unlock(&amp;lock); \/\/ \u0437\u043e\u0432\u0435\u043c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e     return 0; }<\/code><\/pre>\n<p>\u041e\u0434\u043d\u0430\u043a\u043e \u043d\u0430\u0448 \u0431\u0430\u043d\u043a \u0434\u043e\u043b\u0436\u0435\u043d \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c \u043c\u043d\u043e\u0433\u043e \u043b\u044e\u0434\u0435\u0439, \u043f\u043e\u044d\u0442\u043e\u043c\u0443, \u0447\u0442\u043e\u0431\u044b \u0441\u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0435\u0433\u043e \u0440\u0430\u0431\u043e\u0442\u0443, \u043d\u0430\u0434\u043e \u0437\u0430\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 thread \u0432 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u0438\u0445 \u043f\u043e\u0442\u043e\u043a\u0430\u0445 \u043e\u0434\u043d\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u043e:<\/p>\n<pre><code class=\"cpp\">void test() {     ticketlock_init(&amp;lock); \/\/ \u0438\u043d\u0438\u0446\u0438\u0430\u043b\u0438\u0437\u0438\u0440\u0443\u0435\u043c \u043f\u043e\u043b\u044f \u043d\u0443\u043b\u044f\u043c\u0438       thrd_t threads[N_THREADS]; \/\/ \u0441\u043e\u0437\u0434\u0430\u0435\u043c \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u043f\u043e\u0442\u043e\u043a\u043e\u0432     for (int i = 0; i &lt; N_THREADS; ++i) {         int err = thrd_create(&amp;threads[i], thread, NULL); \/\/ \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u0435\u043c \u0432\u043e \u0432\u0441\u0435\u0445 \u043f\u043e\u0442\u043e\u043a\u0430\u0445 thread if (err) {   abort(); }     }      \/\/ \u0441\u043b\u0438\u0432\u0430\u0435\u043c \u043f\u043e\u0442\u043e\u043a\u0438     for (int i = 0; i &lt; N_THREADS; ++i) {         thrd_join(threads[i], NULL);     } }<\/code><\/pre>\n<p>\u041a\u0430\u043a \u043c\u044b \u0445\u043e\u0442\u0438\u043c, \u0447\u0442\u043e\u0431\u044b \u0440\u0430\u0431\u043e\u0442\u0430\u043b\u0430 \u043d\u0430\u0448\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430? \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043d\u0430 \u043f\u0440\u0438\u043c\u0435\u0440\u0435 \u0434\u0432\u0443\u0445 \u043f\u043e\u0442\u043e\u043a\u043e\u0432 (N_THREADS = 2).<\/p>\n<p>\u0411\u0443\u0434\u0435\u043c \u043f\u0440\u0438\u0434\u0435\u0440\u0436\u0438\u0432\u0430\u0442\u044c\u0441\u044f \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0430\u043c\u044f\u0442\u0438 Sequential Consistency (\u0442\u043e \u0435\u0441\u0442\u044c \u043c\u043e\u0436\u043d\u043e \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u043f\u0440\u0438 \u0437\u0430\u043f\u0443\u0441\u043a\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u0438 \u0440\u0430\u0437\u043d\u044b\u0445 \u043f\u043e\u0442\u043e\u043a\u043e\u0432 \u043f\u0435\u0440\u0435\u043c\u0435\u0448\u0438\u0432\u0430\u044e\u0442\u0441\u044f, \u0441\u043e\u0445\u0440\u0430\u043d\u044f\u044f \u0441\u0432\u043e\u0439 \u043f\u043e\u0440\u044f\u0434\u043e\u043a \u0432\u043d\u0443\u0442\u0440\u0438 \u043e\u0434\u043d\u043e\u0433\u043e \u043f\u043e\u0442\u043e\u043a\u0430, \u0438 \u0437\u0430\u043f\u0443\u0441\u043a\u0430\u0435\u0442\u0441\u044f \u043e\u0434\u043d\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0439 \u043a\u043e\u0434).\u00a0<\/p>\n<p>\u0414\u043e\u043f\u0443\u0441\u0442\u0438\u043c \u0432 \u0431\u0430\u043d\u043a \u043f\u0440\u0438\u0448\u043b\u0438 \u041f\u0435\u0442\u044f (\u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a) \u0438 \u0412\u0430\u0441\u044f (\u0432\u0442\u043e\u0440\u043e\u0439 \u043f\u043e\u0442\u043e\u043a). \u0412 \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0441\u0438\u0442\u0443\u0430\u0446\u0438\u0438 \u043e\u043d\u0438 \u043d\u0430\u0445\u043e\u0434\u044f\u0442\u0441\u044f \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u043d\u0430 \u0441\u0442\u0440\u043e\u043a\u0435:<\/p>\n<pre><code class=\"cpp\">ticketlock_lock(&amp;lock);<\/code><\/pre>\n<p>\u041f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0438\u043c, \u0447\u0442\u043e \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a (\u0442\u043e \u0435\u0441\u0442\u044c \u041f\u0435\u0442\u044f \u043f\u0435\u0440\u0432\u044b\u0439 \u0432\u0437\u044f\u043b \u0431\u0438\u043b\u0435\u0442\u0438\u043a):<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next);     atomic_store(&amp;l->next, ticket + 1)<\/code><\/pre>\n<p>\u041e\u043d \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u0431\u0438\u043b\u0435\u0442 \u043d\u043e\u043c\u0435\u0440 0, \u0438 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0431\u0438\u043b\u0435\u0442 \u0431\u0443\u0434\u0435\u0442 \u0443\u0436\u0435 \u0438\u043c\u0435\u0442\u044c \u043d\u043e\u043c\u0435\u0440 1. \u041f\u043e\u0442\u043e\u043c, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0441\u044e\u0434\u0430 \u043c\u043e\u0436\u0435\u0442 \u0432\u0441\u0442\u0440\u043e\u0438\u0442\u044c\u0441\u044f \u0412\u0430\u0441\u0438\u043d (\u0432\u0442\u043e\u0440\u043e\u0439) \u043f\u043e\u0442\u043e\u043a \u0438 \u043e\u0442\u0442\u0443\u0434\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u0442\u0441\u044f \u0442\u0440\u0438 \u0441\u0442\u0440\u043e\u0447\u043a\u0438 (\u0412\u0430\u0441\u044f \u0432\u043e\u0437\u044c\u043c\u0435\u0442 \u0441\u0432\u043e\u0439 \u0431\u0438\u043b\u0435\u0442 \u0438 \u0441\u044f\u0434\u0435\u0442 \u0432 \u043e\u0447\u0435\u0440\u0435\u0434\u044c):<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next); \/\/ \u0412\u0430\u0441\u044f \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u0431\u0438\u043b\u0435\u0442 \u043d\u043e\u043c\u0435\u0440 1 atomic_store(&amp;l->next, ticket + 1); \/\/ \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0431\u0438\u043b\u0435\u0442 \u0442\u0435\u043f\u0435\u0440\u044c \u0438\u043c\u0435\u0435\u0442 \u043d\u043e\u043c\u0435\u0440 2 while (atomic_load(&amp;l->owner) != ticket) { \/\/ owner \u0440\u0430\u0432\u0435\u043d 0, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0412\u0430\u0441\u044f \u0436\u0434\u0435\u0442, \u043f\u043e\u043a\u0430 \u043d\u0435 \u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0438\u0442 \u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c \u041f\u0435\u0442\u0438\u043d \u043f\u043e\u0442\u043e\u043a }<\/code><\/pre>\n<p>\u041d\u0430\u043a\u043e\u043d\u0435\u0446 \u0432\u0441\u0442\u0440\u0430\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a: \u041f\u0435\u0442\u044f \u0441\u043f\u043e\u043a\u043e\u0439\u043d\u043e \u043f\u0435\u0440\u0435\u0441\u043a\u0430\u043a\u0438\u0432\u0430\u0435\u0442 \u0431\u0435\u0441\u043a\u043e\u043d\u0435\u0447\u043d\u044b\u0439 \u0446\u0438\u043a\u043b (\u0430 \u043d\u0435 \u0441\u0430\u0434\u0438\u0442\u0441\u044f \u0442\u0443\u0434\u0430 \u0436\u0434\u0430\u0442\u044c), \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u043d\u043e\u043c\u0435\u0440 \u0435\u0433\u043e \u0431\u0438\u043b\u0435\u0442\u0430 \u0441\u043e\u0432\u043f\u0430\u0434\u0430\u0435\u0442 \u0441 \u043d\u043e\u043c\u0435\u0440\u043e\u043c \u0431\u0438\u043b\u0435\u0442\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0431\u0443\u0434\u0443\u0442 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c.<\/p>\n<pre><code class=\"cpp\"> while (atomic_load(&amp;l->owner) != ticket) { \/\/ \u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u043d\u0435 \u0441\u0440\u0430\u0431\u0430\u0442\u044b\u0432\u0430\u0435\u0442, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e owner = 0, \u0430 \u0443 \u041f\u0435\u0442\u0438 \u043a\u0430\u043a \u0440\u0430\u0437 \u0431\u0438\u043b\u0435\u0442 \u043d\u043e\u043c\u0435\u0440 0  }<\/code><\/pre>\n<p>\u0414\u0430\u043b\u0435\u0435 \u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a \u0432\u044b\u0445\u043e\u0434\u0438\u0442 \u0438\u0437 <code>ticket_lock<\/code> \u0438 \u043d\u0430\u0447\u0438\u043d\u0430\u0435\u0442\u0441\u044f \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u0435 \u041f\u0435\u0442\u0438:<\/p>\n<pre><code class=\"cpp\">int y = x++; \/\/ \u041f\u0435\u0442\u044f \u043f\u043e\u043b\u043e\u0436\u0438\u043b \u0434\u0435\u043d\u0435\u0436\u043a\u0443 \u043d\u0430 \u0441\u0447\u0435\u0442 x assert(x == y + 1); \/\/ \u0432\u0441\u0435 \u0445\u043e\u0440\u043e\u0448\u043e: x = 1, y = 0  ticketlock_unlock(&amp;lock); \/\/ \u0437\u043e\u0432\u0435\u043c \u0412\u0430\u0441\u044e<\/code><\/pre>\n<p>\u0422\u0443\u0442 \u0412\u0430\u0441\u0438\u043d \u043f\u043e\u0442\u043e\u043a \u043d\u0435 \u043c\u043e\u0436\u0435\u0442 \u043d\u0438\u043a\u0443\u0434\u0430 \u0432\u0441\u0442\u0440\u043e\u0438\u0442\u044c\u0441\u044f \u0434\u043e \u0442\u043e\u0433\u043e, \u043a\u0430\u043a \u043c\u044b \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043c <code>ticketlock_unlock(&amp;lock)<\/code>, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u043f\u043e\u043a\u0430 \u0432 \u041f\u0435\u0442\u0438\u043d\u043e\u043c \u043f\u043e\u0442\u043e\u043a\u0435 \u043d\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u0442\u0441\u044f <code>ticketlock_unlock(&amp;lock)<\/code>, \u043d\u043e\u043c\u0435\u0440 \u0412\u0430\u0441\u0438\u043d\u043e\u0433\u043e \u0431\u0438\u043b\u0435\u0442\u0430 (1) \u043d\u0435 \u0441\u043e\u0432\u043f\u0430\u0434\u0435\u0442 \u0441 \u043d\u043e\u043c\u0435\u0440\u043e\u043c \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0435\u043c\u043e\u0433\u043e \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430 (0), \u0438 \u0412\u0430\u0441\u044f \u043d\u0435 \u0441\u043c\u043e\u0436\u0435\u0442 \u0432\u044b\u0439\u0442\u0438 \u0438\u0437 \u0446\u0438\u043a\u043b\u0430 . \u0422\u0430\u043a\u0436\u0435 \u044f\u0441\u043d\u043e, \u0447\u0442\u043e <code>assert<\/code> \u043d\u0435 \u043d\u0430\u0440\u0443\u0448\u0438\u0442\u0441\u044f, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u041f\u0435\u0442\u044f \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 <code>x<\/code> (\u0442\u0430\u043c \u0431\u0443\u0434\u0435\u0442 1, \u0430 \u0432 y \u2014 0), \u043f\u043e\u0442\u043e\u043c \u0442\u043e \u0436\u0435 \u0441\u0430\u043c\u043e\u0435 \u0441\u0434\u0435\u043b\u0430\u0435\u0442 \u0412\u0430\u0441\u044f.<\/p>\n<p>\u042d\u0442\u043e \u0445\u043e\u0440\u043e\u0448\u0435\u0435 \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u0442\u0430\u043a \u043a\u0430\u043a \u0445\u043e\u0442\u044c \u043f\u043e\u0442\u043e\u043a\u0438 \u0438 \u0438\u0441\u043f\u043e\u043b\u043d\u044f\u044e\u0442\u0441\u044f \u043f\u0430\u0440\u0430\u043b\u043b\u0435\u043b\u044c\u043d\u043e, \u043c\u044b \u043d\u0435 \u043c\u043e\u0436\u0435\u043c \u043d\u0430\u0447\u0430\u0442\u044c \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c \u0412\u0430\u0441\u044e, \u043f\u043e\u043a\u0430 \u043d\u0435 \u0437\u0430\u043a\u043e\u043d\u0447\u0438\u043c \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c \u041f\u0435\u0442\u044e.\u00a0<\/p>\n<p>\u0422\u0435\u043f\u0435\u0440\u044c \u0432\u043e\u043f\u0440\u043e\u0441: \u043c\u043e\u0436\u0435\u0442 \u043b\u0438 \u043a\u043e\u0433\u0434\u0430-\u0442\u043e \u043d\u0430\u0440\u0443\u0448\u0438\u0442\u0441\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c\u044b\u0439 <code>assert<\/code>? \u0418 \u043e\u0442\u0432\u0435\u0442: \u043a \u0441\u043e\u0436\u0430\u043b\u0435\u043d\u0438\u044e, \u0434\u0430. \u041d\u0430 \u0441\u0430\u043c\u043e\u043c \u0434\u0435\u043b\u0435 \u044d\u0442\u043e\u0442 <code>assert<\/code> \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f \u0440\u043e\u0432\u043d\u043e \u0442\u043e\u0433\u0434\u0430, \u043a\u043e\u0433\u0434\u0430 \u0432 \u043f\u0440\u043e\u0446\u0435\u0441\u0441 \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u044f \u043e\u0434\u043d\u043e\u0433\u043e \u043a\u043b\u0438\u0435\u043d\u0442\u0430 \u0432\u0441\u0442\u0440\u0430\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u043d\u0438\u0435 \u0434\u0440\u0443\u0433\u043e\u0433\u043e. \u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u043f\u043e\u0441\u043c\u043e\u0442\u0440\u0438\u043c, \u043a\u0430\u043a \u044d\u0442\u043e \u043c\u043e\u0436\u0435\u0442 \u043f\u0440\u043e\u0438\u0437\u043e\u0439\u0442\u0438 \u0432 \u0441\u043b\u0443\u0447\u0430\u0435, \u0435\u0441\u043b\u0438 \u0443 \u043d\u0430\u0441 \u0434\u0432\u0430 \u043f\u043e\u0442\u043e\u043a\u0430.<\/p>\n<p>\u041f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0438\u043c \u0442\u0435\u043f\u0435\u0440\u044c, \u0447\u0442\u043e \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u0432 \u043f\u0435\u0440\u0432\u043e\u043c \u043f\u043e\u0442\u043e\u043a\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u043f\u0435\u0440\u0432\u0430\u044f \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f \u00a0<code>ticketlock_lock<\/code>:<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next);  \/\/ \u041f\u0435\u0442\u044f \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u0431\u0438\u043b\u0435\u0442 \u0441 \u043d\u043e\u043c\u0435\u0440\u043e\u043c 0<\/code><\/pre>\n<p>\u041f\u043e\u0442\u043e\u043c \u0441\u0440\u0430\u0437\u0443 \u0432\u043c\u0435\u0448\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u0432\u0442\u043e\u0440\u043e\u0439 \u043f\u043e\u0442\u043e\u043a, \u0438 \u0442\u0430\u043c \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u044e\u0442\u0441\u044f \u043f\u0435\u0440\u0432\u044b\u0435 \u0434\u0432\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u0438:<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next); \/\/ \u0412\u0430\u0441\u044f \u0442\u043e\u0436\u0435 \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u0442 \u0431\u0438\u043b\u0435\u0442 \u0441 \u043d\u043e\u043c\u0435\u0440\u043e\u043c 0 atomic_store(&amp;l->next, ticket + 1); \/\/ \u043d\u043e\u043c\u0435\u0440 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u043d\u043e\u043c\u0435\u0440\u0430 \u0442\u0435\u043f\u0435\u0440\u044c 1<\/code><\/pre>\n<p>\u041d\u0430\u043a\u043e\u043d\u0435\u0446, \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0430\u044f \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u043f\u043e\u0442\u043e\u043a\u0430:<\/p>\n<pre><code class=\"cpp\">atomic_store(&amp;l->next, ticket + 1); \/\/ \u0432 \u043d\u043e\u043c\u0435\u0440 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u043f\u043e\u0442\u043e\u043a\u0430  \u0441\u043d\u043e\u0432\u0430 \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u0442\u0441\u044f 1<\/code><\/pre>\n<p>\u0414\u0430\u043b\u0435\u0435 \u043d\u0438 \u043e\u0434\u0438\u043d \u0438\u0437 \u043f\u043e\u0442\u043e\u043a\u043e\u0432 \u043d\u0435 \u0437\u0430\u0432\u0438\u0441\u0430\u0435\u0442 \u0432 \u0446\u0438\u043a\u043b\u0435 while, \u0438 \u043e\u043d\u0438 \u043e\u0431\u0430 \u0432\u044b\u0445\u043e\u0434\u044f\u0442 \u0438\u0437 <code>ticketlock_lock<\/code>. \u042d\u0442\u043e \u043f\u043b\u043e\u0445\u043e, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0442\u0435\u043f\u0435\u0440\u044c \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u0441\u043b\u0443\u0447\u0430\u0439\u043d\u043e \u043d\u0430\u0447\u0430\u0442\u044c \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u0432\u0430\u0442\u044c \u0438\u0445 \u043e\u0434\u043d\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u043e, \u0430 \u044d\u0442\u043e \u0438\u043d\u043e\u0433\u0434\u0430 \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 \u043a \u0440\u0430\u0437\u043d\u043e\u0433\u043e \u0440\u043e\u0434\u0430 \u043e\u0448\u0438\u0431\u043a\u0430\u043c (\u0432 \u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, \u043d\u0430\u0440\u0443\u0448\u0435\u043d\u0438\u044f <code>assert<\/code>\u2019a).<\/p>\n<p>\u0421\u043e\u0431\u044b\u0442\u0438\u044f \u043c\u043e\u0433\u0443\u0442 \u0440\u0430\u0437\u0432\u0438\u0432\u0430\u0442\u044c\u0441\u044f \u043a\u0430\u043a-\u0442\u043e \u0442\u0430\u043a: \u0441\u043d\u0430\u0447\u0430\u043b\u0430, \u043f\u0435\u0440\u0432\u044b\u0439 \u043f\u043e\u0442\u043e\u043a \u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0430\u0435\u0442<\/p>\n<pre><code class=\"cpp\">int y = x++; \/\/ \u041f\u0435\u0442\u044f \u043f\u043e\u043b\u043e\u0436\u0438\u043b \u0434\u0435\u043d\u0435\u0436\u043a\u0443 \u043d\u0430 \u0441\u0447\u0435\u0442 x<\/code><\/pre>\n<p>\u0422\u0443\u0442 \u0441\u0440\u0430\u0437\u0443 \u0432\u0441\u0442\u0440\u043e\u0438\u043b\u0441\u044f \u0412\u0430\u0441\u044f:<\/p>\n<pre><code class=\"cpp\">int y = x++; \/\/ \u043e\u0431\u0441\u043b\u0443\u0436\u0438\u043b\u0438 \u0412\u0430\u0441\u044e: \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u043b\u0438 x<\/code><\/pre>\n<p>\u0418 \u0432 \u0438\u0442\u043e\u0433\u0435 \u0432 \u043f\u0435\u0440\u0432\u043e\u043c \u043f\u043e\u0442\u043e\u043a\u0435 \u0432 y \u043d\u0430\u0445\u043e\u0434\u0438\u0442\u0441\u044f 0, \u0430 \u0445 \u0443\u0436\u0435 \u0440\u0430\u0432\u0435\u043d 2, \u0447\u0442\u043e \u0432\u0435\u0434\u0435\u0442 \u043a \u043d\u0435\u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044e <code>assert<\/code>\u2019a.<\/p>\n<p>\u042f\u0441\u043d\u043e, \u0447\u0442\u043e \u0442\u0443\u0442 \u0432\u043e\u0437\u043d\u0438\u043a\u043b\u0430 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0430, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0412\u0430\u0441\u044f \u043f\u043e\u043b\u0443\u0447\u0438\u043b \u0441\u0432\u043e\u0439 \u0431\u0438\u043b\u0435\u0442 \u0434\u043e \u0442\u043e\u0433\u043e, \u043a\u0430\u043a \u043d\u0430\u0448\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430 \u0443\u0441\u043f\u0435\u043b\u0430 \u0434\u043e \u043a\u043e\u043d\u0446\u0430 \u043e\u0431\u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u0438\u0435 \u0431\u0438\u043b\u0435\u0442\u0430 \u041f\u0435\u0442\u0435\u0439. \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u0447\u0442\u043e\u0431\u044b \u0435\u0435 \u0440\u0435\u0448\u0438\u0442\u044c, \u043d\u0430\u0434\u043e \u043f\u0440\u043e\u0441\u0442\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u0442\u0430\u043a, \u0447\u0442\u043e\u0431\u044b \u043e\u0434\u0438\u043d \u043f\u043e\u0442\u043e\u043a \u043d\u0435 \u043c\u043e\u0433 \u0432\u043b\u0435\u0437\u0442\u044c \u043c\u0435\u0436\u0434\u0443 \u0434\u0432\u0443\u043c\u044f \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f\u043c\u0438, \u043e\u0442\u0432\u0435\u0447\u0430\u044e\u0449\u0438\u043c\u0438 \u0437\u0430 \u0432\u044b\u0434\u0430\u0447\u0443 \u0431\u0438\u043b\u0435\u0442\u0430, \u043f\u043e\u043a\u0430 \u0438\u0445 \u0438\u0441\u043f\u043e\u043b\u043d\u044f\u0435\u0442 \u0434\u0440\u0443\u0433\u043e\u0439 \u043f\u043e\u0442\u043e\u043a. \u0410 \u0438\u043c\u0435\u043d\u043d\u043e:<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_load(&amp;l->next); atomic_store(&amp;l->next, ticket + 1);<\/code><\/pre>\n<p>\u0414\u043b\u044f \u044d\u0442\u043e\u0433\u043e \u043c\u043e\u0436\u043d\u043e \u0438\u0445 \u043e\u0431\u044a\u0435\u0434\u0438\u043d\u0438\u0442\u044c \u0432 \u043e\u0434\u043d\u0443 \u0430\u0442\u043e\u043c\u0430\u0440\u043d\u0443\u044e \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044e:<\/p>\n<pre><code class=\"cpp\">int ticket = atomic_fetch_add(&amp;l->next, 1);<\/code><\/pre>\n<p>\u00ab\u041f\u043b\u043e\u0445\u043e\u0439\u00bb \u0441\u043f\u043e\u0441\u043e\u0431<\/p>\n<\/div>\n<\/div>\n<\/div>\n<\/div>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-405567","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/405567","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=405567"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/405567\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=405567"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=405567"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=405567"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}