Диссертация (1149932), страница 27

Файл №1149932 Диссертация (Операционные методы в приложении к слабым моделям памяти) 27 страницаДиссертация (1149932) страница 272019-06-292019-06-29СтудИзба

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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Регистрация/авторизация

Текст из файла (страница 27)

A Program Logic for C11 Memory Fences / M. Doko, V. Vafeiadis //Verification, Model Checking, and Abstract Interpretation — 17th InternationalConference, VMCAI 2016, St. Petersburg, FL, USA, January 17–19, 2016. Proceedings. — 2016. — P. 413–430.89. Vafeiadis, V. Formal Reasoning about the C11 Weak Memory Model /V. Vafeiadis // CPP 2015. — 2015. — P. 1–2.90. Batty, M. Library abstraction for C/C++ concurrency / M. Batty, M. Dodds,A.

Gotsman // POPL 2013. — 2013. — P. 235–248.91. Lidbury, C. Dynamic race detection for C++11 / C. Lidbury, A. F. Donaldson //Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18–20, 2017. — 2017. —P. 443–457.13892. Tassarotti, J. Verifying read-copy-update in a logic for weak memory / J. Tassarotti, D. Dreyer, V. Vafeiadis // Proceedings of the 36th ACM SIGPLAN Conferenceon Programming Language Design and Implementation, Portland, OR, USA, June15–17, 2015. — 2015. — P. 110–120.93.

Doko, M. Tackling Real-Life Relaxed Concurrency with FSL++ / M. Doko,V. Vafeiadis // Programming Languages and Systems — 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April22–29, 2017, Proceedings. — 2017. — P. 448–475.94. Batty, M. — The Thin-air Problem [Электронный ресурс]. — URL: http://www.cl.cam.ac.uk/~pes20/cpp/notes42.html (дата обращения: 29.12.2017).95.

Winskel, G. Event Structures / G. Winskel // Petri Nets: Central Models and TheirProperties, Advances in Petri Nets 1986, Part II, Proceedings of an AdvancedCourse, Bad Honnef, 8.-19. September 1986. — 1986. — P. 325–392.96. Winskel, G. An introduction to event structures / G. Winskel // Linear Time,Branching Time and Partial Order in Logics and Models for Concurrency,School/Workshop, Noordwijkerhout, The Netherlands, May 30 – June 3, 1988,Proceedings.

— 1988. — P. 364–397.97. Tрифанов, В. Динамическое обнаружение состояний гонки в многопоточныхJava-программах: дис. канд. техн. наук: 05.13.11 / В. Tрифанов. — СПб, 2013.— 112 с.98. Подкопаев, А. — Интерпретатор для операционной модели C/++11 [Электронный ресурс]. — URL: https://github.com/anlun/OperationalSemanticsC11(дата обращения: 29.12.2017).99. Bornat, R.

New Lace and Arsenic: adventures in weak memory with a programlogic / R. Bornat, J. Alglave, M. J. Parkinson // CoRR. — 2015. — Vol. abs/1512.01416. — URL: http://arxiv.org/abs/1512.01416.100. Lahav, O. Taming release-acquire consistency / O. Lahav, N. Giannarakis,V. Vafeiadis // Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St.

Petersburg,FL, USA, January 20–22, 2016. — 2016. — P. 649–662.139101. Maranget, L. — 2012. — A Tutorial Introduction to the ARM and POWERRelaxed Memory Models [Электронный ресурс]. — URL: http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf (дата обращения: 29.12.2017).102. Семейство компиляторов GCC [Электронный ресурс]. — URL: https://gcc.gnu.org/ (дата обращения: 29.12.2017).103. Компилятор языка C в платформу LLVM [Электронный ресурс].

— URL:https://clang.llvm.org/ (дата обращения: 29.12.2017).104. McKenney, P. E. Read-Copy Update: Using Execution History to Solve Concurrency Problems / P. E. McKenney, J. D. Slingwine // PDCS. — 1998. — P. 509–518.105. McKenney, P. E. Exploiting Deferred Destruction: An Analysis of Read-CopyUpdate Techniques in Operating System Kernels: Ph.D. thesis / OGI School ofScience and Engineering at Oregon Health and Sciences University. — 2004.106. Desnoyers, M.

User-Level Implementations of Read-Copy Update / M. Desnoyers, P. E. McKenney, A. S. Stern, M. R. Dagenais, J. Walpole // IEEE Transactions on Parallel and Distributed Systems. — 2012. — Feb. — Vol. 23, no. 2. —P. 375–382.107. Hritcu, C. Testing noninterference, quickly / C. Hritcu, J. Hughes, B.

C. Pierce,A. Spector-Zabusky, D. Vytiniotis, A. Azevedo de Amorim, L. Lampropoulos //Proceedings of the 18th ACM SIGPLAN International Conference on FunctionalProgramming (ICFP 2013). — 2013. — P. 455–468.108. Milner, R. Communication and concurrency / R. Milner. PHI Series in computerscience. — Prentice Hall, 1989.109. ARMArchitectureReferenceManual:ARMv8,forARMv8-AArchitectureProfile[Электронныйресурс].—URL:https://developer.arm.com/docs/ddi0487/latest/arm-architecture-reference-manual-armv8-for-armv8-a-architecture-profile(дата обращения: 29.12.2017).140Список рисунков12345678910111213141516171819202122Сценарий программы MP-volatile, который не соответствуетаксиомам модели JMM .

. . . . . . . . . . . . . . . . . . . . . . .Предзапуск программы MP-rel-acq . . . . . . . . . . . . . . . . . .Сценарий поведения программы MP-rel-acq, прошедший базовуюпроверку на корректность . . . . . . . . . . . . . . . . . . . . . .

.Сценарии поведения программы MP-rel-acq в C/C++11 MM . . . .Сценарий поведения программы IF-OOTA-rlx . . . . . . . . . . .. . . 23. . . 27. . . 27. . . 28. . . 28Синтаксис операций и выражений языка модели OpC11 . . . . . . . .Базовые правила OpC11 MM . . . . . . . . . . . .

. . . . . . . . . . .Базовое состояние машины OpC11 . . . . . . . . . . . . . . . . . . . .Правила чтения из неинициализированной локации . . . . . . . . . .Правила высвобождающей записи и приобретающего чтения . . . . .Правила обработки sc-инструкций . . . . . . . . . . . . .

. . . . . .Правила обработки неатомарных обращений и идентификации гонокпо данным . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Правило обработки потребляющего чтения . . . . . . . . . . . . . . .Правила расслабленных обращений . . . . . . . . . . . . . . . .

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

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Реализация алгоритма QSBR RCU . . . . . . . . . . . . . . . . . . . .......474950505152. 53. 54. 55. 58. 59. 60. 60. 64Состояние подсистемы памяти ARMv8 POP при исполнениипрограммы MP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71Состояние подсистемы памяти ARMv8 POP при исполнениипрограммы ARM-weak . .

. . . . . . . . . . . . . . . . . . . . . . . . . 74Состояние подсистем Flowing и POP при исполнении программыWRC-data-addr . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 751412223242526272829Состояния подсистем Flowing и POP при исполнении программыWRC-data-addr (продолжение) . . . . . . . . . . . . . . . .

. . . .Синтаксис программ в модели ARMv8 POP . . . . . . . . . . . . .Состояния подсистемы управления потока в модели ARMv8 POPЯзык состояния исполнения инструкций в ARMv8 POP . . . . . .Функции вычисления состояния переменных regf и regfcom . . . .Переходы обещающей машины . . . . . . . . . . . . . . . .

. . . .Переходы машины ARM+τ . . . . . . . . . . . . . . . . . . . . . ......................768586878993100Сценарий поведения программы MP-sy-ld, запрещённый в моделиARMv8.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113142Список таблиц12Результаты запуска интерпретатора OpC11 MM на “лакмусовых” тестах 63Результаты тестирования модифицированной программы с RCU . . . . 6734Пример состояния подсистемы управления модели ARMv8 POP . .

. . 88Значение функций regf и regfcom для примера из табл. 3 . . . . . . . . . 89143Приложение А. Каталог тестов для модели C/C++11А.1Буферизация записи, SBSB-rel-acq[x] :=rel 0; [y] :=rel 0;[x] :=rel 1; [y] :=rel 1;a :=acq [y] b :=acq [x]Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].SB-sc[x] :=sc 0; [y] :=sc 0;[x] :=sc 1; [y] :=sc 1;a :=sc [y] b :=sc [x]Результаты в C/C++11 MM:[a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].SB-sc-rel[x] :=sc 0; [y] :=sc 0;[x] :=rel 1; [y] :=sc 1;a :=sc [y]b :=sc [x]Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].144SB-sc-acq[x] :=sc 0; [y] :=sc 0;[x] :=sc 1; [y] :=sc 1;a :=acq [y] b :=sc [x]Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].А.2Буферизация чтения, LBLB-rlx[x] :=rlx 0; [y] :=rlx 0;a :=rlx [y] b :=rlx [x][x] :=rlx 1; [y] :=rlx 1;Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].LB-rel-rlx[x] :=rlx 0; [y] :=rlx 0;a :=rlx [y] b :=rlx [x][x] :=rel 1; [y] :=rel 1;Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].LB-acq-rlx[x] :=rlx 0; [y] :=rlx 0;a :=acq [y] b :=acq [x][x] :=rlx 1; [y] :=rlx 1;Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].145LB-rel-acq-rlx[x] :=rlx 0; [y] :=rlx 0;a :=acq [y] b :=rlx [x][x] :=rlx 1; [y] :=rel 1;Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0].LB-rlx-use[x] :=rlx 0; [y] :=rlx 0;a :=rlx [y]b :=rlx [x][z1] :=rlx a; [z2] :=rlx b;[x] :=rlx 1; [y] :=rlx 1;Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].LB-rlx-let[x] :=rlx 0; [y] :=rlx 0;a :=rlx [y] b :=rlx [x]a′ := a + 1; b′ := b + 1;[x] :=rlx 1; [y] :=rlx 1;Результаты в C/C++11 MM:[a = 0, a′ = 1, b = 0, b′ = 1], [a = 0, a′ = 1, b = 1, b′ = 2],[a = 1, a′ = 2, b = 0, b′ = 1], [a = 1, a′ = 2, b = 1, b′ = 2].146LB-rlx-join[x] :=rlx 0; [y] :=rlx 0;a :=rlx [y]; skip b :=rlx [x]; skip[z1] :=rlx a[z2] :=rlx b[x] :=rlx 1[y] :=rlx 1Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].LB-rel-rlx-join[x] :=rlx 0; [y] :=rlx 0;a :=rlx [y]; skip b :=rlx [x]; skip[z1] :=rlx a[z2] :=rlx b[x] :=rel 1[y] :=rel 1Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].LB-acq-rlx-join[x] :=rlx 0; [y] :=rlx 0;a :=acq [y]; skip b :=acq [x]; skip[z1] :=rlx a[z2] :=rlx b[x] :=rlx 1[y] :=rlx 1Результаты в C/C++11 MM:[a = 0, b = 0], [a = 0, b = 1], [a = 1, b = 0], [a = 1, b = 1].147А.3Передача сообщения, MPMP-rlx-na[f ] :=rlx 0; [d] :=na 0;[d] :=na 5; repeat [f ]rlx end;[f ] :=rlx 1 a :=na [d]Результаты в C/C++11 MM:undefined behavior.MP-rel-rlx-na[f ] :=rlx 0; [d] :=na 0;[d] :=na 5; repeat [f ]rlx end;[f ] :=rel 1 a :=na [d]Результаты в C/C++11 MM:undefined behavior.MP-rlx-acq-na[f ] :=rlx 0; [d] :=na 0;[d] :=na 5; repeat [f ]acq end;[f ] :=rlx 1 a :=na [d]Результаты в C/C++11 MM:undefined behavior.MP-rel-acq-na[f ] :=rlx 0; [d] :=na 0;[d] :=na 5; repeat [f ]acq end;[f ] :=rel 1 a :=na [d]Результаты в C/C++11 MM:[a = 5].148MP-rel-acq-na-rlx[f ] :=rel 0; [d] :=na 0;[d] :=na 5;repeat [f ]acq == 2 end;[f ] :=rel 1; a :=na [d][f ] :=rlx 2Результаты в C/C++11 MM:[a = 5].MP-rel-acq-na-rlx_2[d][f ][x][f ][f ] :=na 0; [d] :=na 0; [x] :=na 0;:=na 5;repeat [f ]acq == 2 end;:=rel 1; a :=na [d]:=rel 1; b :=rlx [x]:=rlx 2Результаты в C/C++11 MM:[a = 5, b = 0], [a = 5, b = 1].MP-con-na[f ] :=rlx null; [d] :=na 0;[d] :=na 5; a :=con [f ];if a ̸= nullthen b :=na [a][f ] :=rel delse b := 0fiРезультаты в C/C++11 MM:[a = null, b = 0], [a = d, b = 5].149MP-con-na_2[p] :=na null; [d] :=na 0; [x] :=na 0;a :=con [p];if a ̸= null[x] :=rlx 1;then b :=na [a];[d] :=na 1;c :=rlx [x][p] :=rel delse b := 0; c := 0fiРезультаты в C/C++11 MM:[a = null, b = 0, c = 0], [a = d, b = 5, c = 0], [a = d, b = 5, c = 1].MP-cas-rel-acq-na[d] :=na 5;[f ] :=rel 0[f ] :=rlx 1; [d] :=na 0;a := casacq,rlx (f, 0, 1); b := casacq,rlx (f, 0, 1);if a == 0if b == 0then [d] :=rlx 6then [d] :=rlx 7else 0else 0fifiРезультаты в C/C++11 MM:[a = 0, b = 1], [a = 1, b = 0].MP-cas-rel-rlx-na[d] :=na 5;[f ] :=rel 0[f ] :=rlx 1; [d] :=na 0;a := casrlx,rlx (f, 0, 1); b := casrlx,rlx (f, 0, 1);if a == 0if b == 0then [d] :=rlx 6then [d] :=rlx 7else 0else 0fifiРезультаты в C/C++11 MM:undefined behavior.150А.4Корректность повторного чтения, CoRRCoRR-rlx[x] :=rlx 1[x] :=rlx 0;a :=rlx [x];[x] :=rlx 2b :=rlx [x]c :=rlx [x];d :=rlx [x]В C/C++11 MM возможны все результаты, соответствующие {a, b, c, d} ⊆{0, 1, 2}, кроме тех, в которых a > b = 0 или c > d = 0, а также[a = 1, b = 2, c = 2, d = 1], [a = 2, b = 1, c = 1, d = 2].CoRR-rel-acq[x] :=rel 1[x] :=rel 0;a :=acq [x];[x] :=rel 2b :=acq [x]c :=acq [x];d :=acq [x]В C/C++11 MM возможны все результаты, соответствующие {a, b, c, d} ⊆{0, 1, 2}, кроме тех, в которых a > b = 0 или c > d = 0, а также[a = 1, b = 2, c = 2, d = 1], [a = 2, b = 1, c = 1, d = 2].А.5Независимые чтения независимых записей, IRIWIRIW-rlx[x] :=rlx 1[x] :=rlx 0; [y] :=rlx 0;[y] :=rlx 1 a :=rlx [x];b :=rlx [y]c :=rlx [y];d :=rlx [x]В C/C++11 MM возможны все результаты, соответствующие {a, b, c, d} ⊆{0, 1}.151IRIW-rel-acq[x] :=rel 1[x] :=rel 0; [y] :=rel 0;[y] :=rel 1 a :=acq [x];b :=acq [y]c :=acq [y];d :=acq [x]В C/C++11 MM возможны все результаты, соответствующие {a, b, c, d} ⊆{0, 1}.IRIW-sc[x] := 1[x] := 0; [y] := 0;[y] := 1 a := [x];b := [y]c := [y];d := [x]В C/C++11 MM возможны все результаты, соответствующие {a, b, c, d} ⊆{0, 1}, кроме [a = 1, b = 0, c = 1, d = 0].А.6Зависимость запись-чтение, WRCWRC-rel-acq[x] :=rel 0; [y] :=rel 0;[x] :=rel 1 a :=acq [x]; b :=acq [y];[y] :=rel a c :=acq [x]Результаты в C/C++11 MM:[a = 0, b = 0, c = 0], [a = 1, b = 0, c = 0],[a = 1, b = 0, c = 1], [a = 1, b = 1, c = 1].152WRC-rlx[x] :=rlx 0; [y] :=rlx 0;[x] :=rlx 1 a :=rlx [x]; b :=rlx [y];[y] :=rlx a c :=rlx [x]Результаты в C/C++11 MM:[a = 0, b = 0, c = 0], [a = 1, b = 0, c = 0],[a = 1, b = 0, c = 1], [a = 1, b = 1, c = 1],[a = 1, b = 1, c = 0].WRC-cas-rel[x] :=rel[y] :=rel[x] :=rel 0; [y] :=rel 0;1; a := casrel,acq (y, 1, 2) b :=acq [y];1c :=acq [x]Результаты в C/C++11 MM:[a = 0, b = 0, c = 0], [a = 1, b = 0, c = 0],[a = 1, b = 0, c = 1], [a = 1, b = 0, c = 1],[a = 1, b = 1, c = 1], [a = 1, b = 1, c = 1],[a = 1, b = 2, c = 1].WRC-cas-rlx[x] :=rlx[y] :=rel[x] :=rlx 0; [y] :=rlx 0;1; a := casrlx,rlx (y, 1, 2) b :=acq [y];1c :=rlx [x]Результаты в C/C++11 MM:[a = 0, b = 0, c = 0], [a = 1, b = 0, c = 0],[a = 1, b = 0, c = 1], [a = 1, b = 0, c = 1],[a = 1, b = 1, c = 1], [a = 1, b = 1, c = 1],[a = 1, b = 2, c = 1].153А.7“Значения из воздуха”, OOTAOTA-lb[x] :=rlx 0; [y] :=rlx 0;a :=rlx [y]; b :=rlx [x][x] :=rlx a; [y] :=rlx bC/C++11 MM разрешает для этой программы любой результат, в которомa = b.OTA-if[x] :=rlx 0; [y] :=rlx 0;a :=rlx [y];b :=rlx [x];if aif bthen [x] :=rlx 1then [y] :=rlx 1else a := 0else b := 0fifiРезультаты в C/C++11 MM:[a = 0, b = 0], [a = 1, b = 1].А.8Независимые записи, WRWR-rlx[x] :=rlx 0; [y] :=rlx 0;[x] :=rlx 1; [y] :=rlx 1;[y] :=rlx 2 [x] :=rlx 2a :=rlx [x]; b :=rlx [y]Результаты в C/C++11 MM:[a = 1, b = 2], [a = 1, b = 2], [a = 1, b = 2], [a = 2, b = 2].154WR-rlx-rel[x] :=rlx 0; [y] :=rlx 0;[x] :=rlx 1; [y] :=rlx 1;[y] :=rel 2 [x] :=rel 2a :=rlx [x]; b :=rlx [y]Результаты в C/C++11 MM:[a = 1, b = 2], [a = 1, b = 2], [a = 1, b = 2], [a = 2, b = 2].WR-rel[x] :=rel 0; [y] :=rel 0;[x] :=rel 1; [y] :=rel 1;[y] :=rel 2 [x] :=rel 2a :=acq [x]; b :=acq [y]Результаты в C/C++11 MM:[a = 1, b = 2], [a = 1, b = 2], [a = 1, b = 2], [a = 2, b = 2].А.9Спекулятивное исполнение, SESE-simple[x] :=rlx 0; [y] :=rlx 0; [z] :=rlx 0;a :=rlx [x];b :=rlx [y];if aif bthen [z] :=rlx 1;then [x] :=rlx 1[y] :=rlx 1else skipelse [y] :=rlx 1fific :=rlx [z]Результаты в C/C++11 MM:[a = 0, b = 0, c = 0], [a = 0, b = 1, c = 0],[a = 1, b = 1, c = 1].155SE-prop[x] :=rlx 0; [y] :=rlx 0; [z] :=rlx 0;a :=rlx [x];if ab :=rlx [y];then [z] :=rlx 1;if ba :=rlx [z];then [x] :=rlx 1[y] :=rlx aelse skipelse [y] :=rlx 1fific :=rlx [z]Результаты в C/C++11 MM:[a = 0, b = 0, c = 0], [a = 0, b = 1, c = 0],[a = 1, b = 1, c = 1].SE-nested[x] :=rlx 0; [y] :=rlx 0; [z] :=rlx 0; [f ] :=rlx 0;a :=rlx [x];if athen d :=rlx [f ];b :=rlx [y];if dif athen [z] :=rlx 1;then [f ] :=rlx 1;[y] :=rlx 1[x] :=rlx 1else [y] :=rlx 1else skipfifielse [y] :=rlx 1fic :=rlx [z]Результаты в C/C++11 MM:[a = 0, b = 0, c = 0, d = ⊥], [a = 0, b = 1, c = 0, d = ⊥],[a = 1, b = 1, c = 0, d = 0], [a = 1, b = 1, c = 1, d = 1].156А.10ARM-weak[x] := 0; [y] := 0;a := [x]; //1 b := [x]; c := [y];[x] := 1[y] := b [x] := cРезультаты в C/C++11 MM:[a = 0, b = 0, c = 0], [a = 0, b = 1, c = 0], [a = 0, b = 1, c = 1], [a = 1, b = 1, c = 1].А.11 БлокировкиБлокировка Деккера[x] :=rel 0; [y] :=rel 0; [d] :=na 0;[x] :=rel 1;[y] :=rel 1;a :=acq [y];b :=acq [x];if a == 0if b == 0then [d] :=na 5then [d] :=na 6else skipelse skipfifiРезультаты в C/C++11 MM:undefined behavior.157Блокировка Коэна [66][x] :=rel 0; [y] :=rel 0; [d] :=na 0;[x] :=rel choice 1 2; [y] :=rel choice 1 2;repeat [y]acq end;repeat [x]acq end;a :=acq [x];c :=acq [x];b :=acq [y];d :=acq [y];if a == bif c ̸= dthen [d] :=na 5then [d] :=na 6else skipelse skipfifiРезультаты в C/C++11 MM:[a = 1, b = 1, c = 1, d = 1], [a = 1, b = 2, c = 1, d = 2],[a = 2, b = 1, c = 2, d = 1], [a = 2, b = 2, c = 2, d = 2].158Приложение Б.

Характеристики

Тип файла

PDF-файл

Размер

763,31 Kb

Материал

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

Тип материала

Кандидатская диссертация

Предмет

Физико-математические науки

Высшее учебное заведение

СПбГУ

Список файлов диссертации

operacionnye-metody-v-prilozhenii-k-slabym-modeljam-pamjati.rar

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

Автореферат.pdf

Выписка из протокола заседания диссертационного совета.pdf

Диссертация.pdf

Информация об официальном оппоненте 2.pdf

Информация об официальном оппоненте.pdf

Отзыв ведущей организации.pdf

Отзыв на автореферат 2.pdf

Отзыв на автореферат 3.pdf

Отзыв на автореферат 4.pdf

Отзыв на автореферат 5.pdf

Отзыв на автореферат.pdf

Отзыв научного руководителя.pdf

Отзыв официального оппонента 2.pdf

Отзыв официального оппонента.pdf

Прочти меня!!!.txt

Сведения о ведущей организации.pdf

Сведения о результатах публичной защиты.pdf

Поделитесь ссылкой:

Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.

Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.

Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.

Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.

Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.

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

Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.

Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.

Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.

Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.

Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.

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