A Methodology for Opacity verification for Transactional Memory algorithms using Graph Transformation System
Resumo
Com a constante pesquisa e desenvolvimento de sistemas de Memória Transacional (TM), vários algoritmos têm sido propostos, e sua corretude é sempre um aspecto importante a se levar em consideração. Ao analisar algoritmos de TM, um dos critérios de corretude mais comumente usados é opacidade, que infere que execuções só observam estados consistentes da memória compartilhada. Este artigo propõe uma definição formal para demonstrar que um determinado algoritmo TM só gera histórias opacas usando um Sistema de Transformação de Grafos. Uma metodologia é introduzida para traduzir um algoritmo para regras de produção que manipulam o estado de um grafo. A abordagem proposta demonstrou a capacidade de lidar com algumas das complexidades de algoritmos TM e um caso de estudo mostra o funcionamento da prova de opacidade do algoritmo em questão.
Palavras-chave:
Transactional Memory, Opacity, Algorithm, Graph Transformation System, Formalism
Referências
Bushkov, V., Dziuma, D., Fatourou, P., and Guerraoui, R. (2018). The pcl theorem: Transactions cannot be parallel, consistent, and live. Journal of the ACM (JACM), 66.
Cardoso, D. J., Foss, L., and Bois, A. R. D. (2019). A graph transformation system formalism for software transactional memory opacity. In Proceedings of the XXIII Brazilian Symposium on Programming Languages, pages 3–10.
Cardoso, D., Foss, L., and Du Bois, A. (2021). A graph transformation system formalism for correctness of transactional memory algorithms. In 25th Brazilian Symposium on Programming Languages, pages 49–57.
Guerraoui, R. and Kapalka, M. (2008). On the correctness of transactional memory. In Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming, pages 175–184.
Guerraoui, R. and Kapałka, M. (2010). Principles of transactional memory. Synthesis Lectures on Distributed Computing, 1(1):1–193.
Harris, T., Marlow, S., Peyton-Jones, S., and Herlihy, M. (2005). Composable memory transactions. In Proceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’05, pages 48–60, New York, NY, USA.
Herlihy, M. and Moss, J. E. B. (1993).Transactional memory: Architectural support forlock-free data structures, volume 21. ACM.
Khyzha, A., Attiya, H., Gotsman, A., and Rinetzky, N. (2018). Safe privatization in transactional memory.ACM SIGPLAN, 53:233–245.
Lesani, M. and Palsberg, J. (2014). Decomposing opacity. In International Symposiumon Distributed Computing, pages 391–405. Springer.
Maric, O. (2017).Formal Verification of Fault-Tolerant Systems. PhD thesis, ETH Zurich.
Matveev, A. and Shavit, N. (2015). Reduced hardware norec: A safe and scalable hybridtm. In ACM SIGARCH Computer Architecture News, volume 43, pages 59–71.
Pankratius, V. and Adl-Tabatabai, A.-R. (2011). A study of transactional memory vs.locks in practice. In Proceedings of the twenty-third annual ACM symposium on Parallelism in algorithms and architectures, pages 43–52. ACM.
Peluso, S., Palmieri, R., Romano, P., Ravindran, B., and Quaglia, F. (2015). Disjoint-access parallelism: Impossibility, possibility, and cost of TM implementations. In Proce. of the 2015 ACM Symp. on Principles of Distri. Computing, pages 217–226.
Peterson, C. and Dechev, D. (2017). A transactional correctness tool for abstract datatypes. ACM Transactions on Architecture and Code Optimization, 14(4):1–24.
Shavit, N. and Touitou, D. (1997). Software transactional memory. Distributed Computing, 10:99–116.
Wamhoff, J.-T., Riegel, T., Fetzer, C., and Felber, P. (2010). Robustm: A robust software tm. In Symp. on Self-Stabilizing Systems, pages 388–404.
Cardoso, D. J., Foss, L., and Bois, A. R. D. (2019). A graph transformation system formalism for software transactional memory opacity. In Proceedings of the XXIII Brazilian Symposium on Programming Languages, pages 3–10.
Cardoso, D., Foss, L., and Du Bois, A. (2021). A graph transformation system formalism for correctness of transactional memory algorithms. In 25th Brazilian Symposium on Programming Languages, pages 49–57.
Guerraoui, R. and Kapalka, M. (2008). On the correctness of transactional memory. In Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming, pages 175–184.
Guerraoui, R. and Kapałka, M. (2010). Principles of transactional memory. Synthesis Lectures on Distributed Computing, 1(1):1–193.
Harris, T., Marlow, S., Peyton-Jones, S., and Herlihy, M. (2005). Composable memory transactions. In Proceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’05, pages 48–60, New York, NY, USA.
Herlihy, M. and Moss, J. E. B. (1993).Transactional memory: Architectural support forlock-free data structures, volume 21. ACM.
Khyzha, A., Attiya, H., Gotsman, A., and Rinetzky, N. (2018). Safe privatization in transactional memory.ACM SIGPLAN, 53:233–245.
Lesani, M. and Palsberg, J. (2014). Decomposing opacity. In International Symposiumon Distributed Computing, pages 391–405. Springer.
Maric, O. (2017).Formal Verification of Fault-Tolerant Systems. PhD thesis, ETH Zurich.
Matveev, A. and Shavit, N. (2015). Reduced hardware norec: A safe and scalable hybridtm. In ACM SIGARCH Computer Architecture News, volume 43, pages 59–71.
Pankratius, V. and Adl-Tabatabai, A.-R. (2011). A study of transactional memory vs.locks in practice. In Proceedings of the twenty-third annual ACM symposium on Parallelism in algorithms and architectures, pages 43–52. ACM.
Peluso, S., Palmieri, R., Romano, P., Ravindran, B., and Quaglia, F. (2015). Disjoint-access parallelism: Impossibility, possibility, and cost of TM implementations. In Proce. of the 2015 ACM Symp. on Principles of Distri. Computing, pages 217–226.
Peterson, C. and Dechev, D. (2017). A transactional correctness tool for abstract datatypes. ACM Transactions on Architecture and Code Optimization, 14(4):1–24.
Shavit, N. and Touitou, D. (1997). Software transactional memory. Distributed Computing, 10:99–116.
Wamhoff, J.-T., Riegel, T., Fetzer, C., and Felber, P. (2010). Robustm: A robust software tm. In Symp. on Self-Stabilizing Systems, pages 388–404.
Publicado
17/11/2021
Como Citar
CARDOSO, Diogo J.; FOSS, Luciana; DU BOIS, Andre R..
A Methodology for Opacity verification for Transactional Memory algorithms using Graph Transformation System. In: WORKSHOP-ESCOLA DE INFORMÁTICA TEÓRICA (WEIT), 6. , 2021, Online.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2021
.
p. 9-16.
DOI: https://doi.org/10.5753/weit.2021.18916.
