Генерация перестановок частично упорядоченного множества с учётом зависимости в элементах
Аннотация
Данная работа посвящена разработке методов, позволяющих существенно сократить количество линейных порядков, необходимых для анализа частично упорядоченных множеств. Такой анализ играет ключевую роль при тестировании многопоточных систем, где важно учитывать все допустимые варианты межпоточного взаимодействия. В настоящее время для тестирования подобных систем применяются как направленные литмус-тесты, специально сконструированные для проверки конкретных эффектов, так и генераторы последовательностей инструкций, порождающие рандомизированные, но простые и удобные для проверки, сценарии исполнения с существенными ограничениями. Применение сложных случайных входных данных затруднено из-за экспоненциального роста числа линейных порядков для анализа. Предлагаемый в данной работе алгоритм позволяет существенно сократить число рассматриваемых линейных порядков за счёт учёта зависимостей между элементами множества при их переупорядочивании. Полученные результаты делают возможным более эффективное тестирование многопоточных систем и расширяют область применения методов анализа частичного порядка.
Литература
2. Madduri K., Feo J., Cong G., Bader D.A. Design of Multithreaded Algorithms for Combinatorial Problems. In: Rajasekaran S., Reif J.H. (eds) Handbook of Parallel Computing – Models, Algorithms and Applications. Chapman and Hall/CRC; 2007. p. 787-816. https://doi.org/10.1201/9781420011296.ch31
3. Petrochenkov M., Stotland I., Mushtakov R. Approaches to Stand-alone Verification of Multicore Microprocessor Caches. Trudy ISP RAN = Proceedings of the Institute for System Programming of the RAS. 2016;28(3):161-172. https://doi.org/10.15514/ISPRAS-2016-28(3)-10
4. Bennett A.J., Field T., Harrison P. Modelling and validation of shared memory coherency protocols. Performance evaluation. 1996;27-28:541-563. https://doi.org/10.1016/S0166-5316(96)90045-0
5. Petrot F., Greiner A., Gomez P. On Cache Coherency and Memory Consistency Issues in NoC Based Shared Memory Multiprocessor SoC Architectures. In: Proceedings of the 9th EUROMICRO Conference on Digital System Design (DSD '06). IEEE Computer Society, USA; 2006. p. 53-60. https://doi.org/10.1109/DSD.2006.73
6. Björner A., Wachs M.L. Permutation statistics and linear extensions of posets. Journal of Combinatorial Theory, Series A. 1991;58(1):85-114. https://doi.org/10.1016/0097-3165(91)90075-R
7. Hangal S., Vahia D., Manovit C., Lu J.-Y.J. TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model. ACM SIGARCH Computer Architecture News. 2004;32(2):114. https://doi.org/10.1145/1028176.1006710
8. Naylor M., Moore S.W., Mujumdar A. A consistency checker for memory subsystem traces. In: Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design (FMCAD '16). Austin, Texas: FMCAD Inc; 2016. p. 133-140.
9. Wagner, Chin, McCluskey. Pseudorandom Testing. IEEE Transactions on Computers. 1987;C-36(3):332-343. https://doi.org/10.1109/TC.1987.1676905
10. Mador-Haim S., Alur R., Martin M.M.K. Litmus tests for comparing memory consistency models: how long do they need to be? In: Proceedings of the 48th Design Automation Conference (DAC '11). New York, NY, USA: Association for Computing Machinery; 2011. p. 504-509. https://doi.org/10.1145/2024724.2024842
11. Mador-Haim S., Alur R., Martin M.M.K. Generating Litmus Tests for Contrasting Memory Consistency Models. In: Touili T., Cook B., Jackson P. (eds.) Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science. Vol. 6174. Berlin, Heidelberg: Springer; 2010. p. 273-287. https://doi.org/10.1007/978-3-642-14295-6_26
12. Kangas K., Hankala T., Niinimaki T., Koivisto M. Counting Linear Extensions of Sparse Posets. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI'16). New York, New York, USA: AAAI Press, 2016. p. 603-609.
13. Kahn A.B. Topological sorting of large networks. Communications of the ACM. 1962;5(11):558-562. https://doi.org/10.1145/368996.369025
14. Brightwell G., Winkler P. Counting linear extensions. Order. 1991;8:225-242. https://doi.org/10.1007/BF00383444
15. Knuth D. Permutations, matrices, and generalized Young tableaux. Pacific Journal of Mathematics. 1970;34(3):709-727.
16. Haiman M.D. Dual equivalence with applications, including a conjecture of Proctor. Discrete Mathematics. 1992;99(1-3):79-113.
17. Robinson G. de B. On the representations of the symmetric group. American Journal of Mathematics. 1938:745-760.
18. Andreev I.V., Vladimirov K.I. Efficient Reordering of Multiple Memory Operations in a Multithreaded Program. Modern Information Technologies and IT-Education. 2024;20(1):149-156. (In Russ., abstract in Eng.) https://doi.org/10.25559/SITITO.020.202401.149-156
19. Andreev I.V., Vladimirov K.I. Efficient Reordering of Multiple Memory Operations in a Multithreaded Program. Modern Information Technologies and IT-Education. 2024;20(1):149-156. (In Russ., abstract in Eng.) https://doi.org/10.25559/SITITO.020.202401.149-156
20. Hendry G.R.T. Extending cycles in graphs. Discrete Mathematics. 1990;85(1):59-72. https://doi.org/10.1016/0012-365X(90)90163-C
21. Corneil D.G., Lerchs H., Burlingham L.S. Complement reducible graphs. Discrete Applied Mathematics. 1981;3(3):163-174.
22. Beineke L.W., Harary F. The thickness of the complete graph. Canadian Journal of Mathematics. 1965;17:850-859.
23. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE transactions on computers. 1979;C-28(9):690-691. https://doi.org/10.1109/TC.1979.1675439
24. Oberhauser J. Store Buffer Reduction in the Presence of Mixed-Size Accesses and Misalignment. In: Piskac R., Rümmer P. (eds.) Verified Software. Theories, Tools, and Experiments. VSTTE 2018. Lecture Notes in Computer Science. Vol. 11294. Cham: Springer; 2018. p. 322-344. https://doi.org/10.1007/978-3-030-03592-1_19
25. Cohen E., Schirmer B. From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. In: Kaufmann M., Paulson L.C. (eds.) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science. Vol. 6172. Berlin, Heidelberg: Springer; 2010. p. 403-418. https://doi.org/10.1007/978-3-642-14052-5_28
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.
Редакционная политика журнала основывается на традиционных этических принципах российской научной периодики и строится с учетом этических норм работы редакторов и издателей, закрепленных в Кодексе поведения и руководящих принципах наилучшей практики для редактора журнала (Code of Conduct and Best Practice Guidelines for Journal Editors) и Кодексе поведения для издателя журнала (Code of Conduct for Journal Publishers), разработанных Комитетом по публикационной этике - Committee on Publication Ethics (COPE). В процессе издательской деятельности редколлегия журнала руководствуется международными правилами охраны авторского права, нормами действующего законодательства РФ, международными издательскими стандартами и обязательной ссылке на первоисточник.
Журнал позволяет авторам сохранять авторское право без ограничений. Журнал позволяет авторам сохранить права на публикацию без ограничений.
Издательская политика в области авторского права и архивирования определяются «зеленым цветом» в базе данных SHERPA/RoMEO.
Все статьи распространяются на условиях лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная, которая позволяет другим использовать, распространять, дополнять эту работу с обязательной ссылкой на оригинальную работу и публикацию в этом журналe.
