{"id":234,"date":"2024-04-23T15:59:35","date_gmt":"2024-04-23T15:59:35","guid":{"rendered":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/?p=234"},"modified":"2024-04-23T15:59:35","modified_gmt":"2024-04-23T15:59:35","slug":"un-nuevo-enfoque-de-la-programacion-concurrente-garantiza-la-correccion-de-los-programas-informaticos","status":"publish","type":"post","link":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/2024\/04\/23\/un-nuevo-enfoque-de-la-programacion-concurrente-garantiza-la-correccion-de-los-programas-informaticos\/","title":{"rendered":"Un nuevo enfoque de la programaci\u00f3n concurrente garantiza la correcci\u00f3n de los programas inform\u00e1ticos"},"content":{"rendered":"
\"El
El investigador Joakim \u00d6hman en las instalaciones del Instituto IMDEA Software<\/figcaption><\/figure>\n

El investigador Joakim \u00d6hman, supervisado por el profesor Aleks Nanevski<\/a>, present\u00f3 su tesis: \u00abCompositional Reasoning of Concurrency with the Visibility Method<\/strong>\u00bb el pasado 15 de abril en el Instituto IMDEA Software, acompa\u00f1ado de colegas y familiares.<\/p>\n

Para mejorar a\u00fan m\u00e1s la eficiencia y la velocidad de los programas inform\u00e1ticos en la era posterior al escalado de Dennard, es esencial el desarrollo de programas concurrentes. Los programas concurrentes constan de m\u00faltiples procedimientos que se ejecutan en paralelo, los llamados hilos, que en alg\u00fan momento necesitan sincronizarse para producir un resultado unificado. La elecci\u00f3n de la sincronizaci\u00f3n determina en gran medida la capacidad de ejecuci\u00f3n concurrente del programa, influyendo as\u00ed en su eficiencia.<\/p>\n

La tesis desvela un enfoque modular para demostrar la linealidad de los algoritmos de instant\u00e1neas concurrentes<\/strong>, mejorando significativamente nuestra comprensi\u00f3n y formalizando conceptos hasta ahora informales. La linealizabilidad garantiza efectivamente que un algoritmo concurrente se comporta correctamente, de forma que se puede sustituir un algoritmo secuencial por uno concurrente sin problemas, sin que se produzcan desviaciones en el funcionamiento. **Sin una prueba de linealidad, un algoritmo puede comportarse de forma inesperada y presentar errores**, sobre todo teniendo en cuenta la imprevisibilidad inherente a la concurrencia.<\/p>\n

Joakim present\u00f3 pruebas modulares para tres algoritmos de instant\u00e1nea desarrollados por Jayanti y uno por Afek et al., todos ellos logrados mediante el uso innovador del razonamiento de visibilidad, introducido originalmente por Henzinger et al. En un intento de racionalizar el proceso de prueba, las pruebas de linealidad se desmontaron en m\u00f3dulos de prueba individuales. Cabe destacar que un n\u00famero considerable de estos m\u00f3dulos se compartieron en los tres algoritmos, lo que hace hincapi\u00e9 en la eficiencia al desarrollarlos una vez y reutilizarlos varias veces para reducir la complejidad de las pruebas<\/strong>.<\/p>\n

El quid de este avance reside en las interfaces de los m\u00f3dulos, compuestas por relaciones y axiomas. Un m\u00f3dulo, en particular, encapsula el concepto fundamental de \u00abreenv\u00edo\u00bb que constituye la espina dorsal del dise\u00f1o de Jayanti. Este trabajo ha demostrado con \u00e9xito que un formalismo basado en el razonamiento de visibilidad puede captar con habilidad estos intrincados principios, que hasta ahora s\u00f3lo hab\u00edan sido articulados informalmente por Jayanti en ingl\u00e9s.<\/p>\n

A diferencia de los enfoques convencionales de simulaci\u00f3n de la linealidad, el enfoque de la visibilidad se centra en la determinaci\u00f3n de los elementos esenciales necesarios para establecer la linealidad. Sin embargo, determinar estos elementos esenciales para estructuras de datos con un orden parcial arbitrario de operaciones puede plantear retos formidables.<\/p>\n

En una mezcla estrat\u00e9gica de metodolog\u00edas, esta investigaci\u00f3n aprovech\u00f3 ideas de ambos enfoques. Al asumir un orden total entre operaciones espec\u00edficas, se racionaliz\u00f3 la tarea de identificar los elementos esenciales para la linealidad. Esta amalgama result\u00f3 crucial, ya que desarrollar una especificaci\u00f3n coherente de la estructura de instant\u00e1neas sin presuponer un orden total entre los escritores de la misma c\u00e9lula result\u00f3 ser una ardua tarea.<\/p>\n

Esta innovadora investigaci\u00f3n no s\u00f3lo perfecciona la comprensi\u00f3n de los algoritmos de instant\u00e1nea<\/strong>, sino que tambi\u00e9n muestra el potencial del razonamiento de visibilidad como herramienta robusta para formalizar conceptos complejos de programaci\u00f3n concurrente.<\/p>\n","protected":false},"excerpt":{"rendered":"

El investigador Joakim \u00d6hman, supervisado por el profesor Aleks Nanevski, present\u00f3 su tesis: \u00abCompositional Reasoning of Concurrency with the Visibility Method\u00bb el pasado 15 de abril en el Instituto IMDEA Software, acompa\u00f1ado de colegas y familiares. Para mejorar a\u00fan m\u00e1s la eficiencia y la velocidad de los programas inform\u00e1ticos en la era posterior al escalado de Dennard, es esencial el desarrollo de programas concurrentes. Los programas concurrentes constan de m\u00faltiples procedimientos que se ejecutan en paralelo, los llamados hilos, que en alg\u00fan momento necesitan sincronizarse para producir un resultado unificado. La elecci\u00f3n de la sincronizaci\u00f3n determina en gran medida la\u2026<\/p>\n","protected":false},"author":243,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"ngg_post_thumbnail":0},"categories":[7197],"tags":[51830,51832,22421,135,51831,244,51779,51833],"blocksy_meta":{"styles_descriptor":{"styles":{"desktop":"","tablet":"","mobile":""},"google_fonts":[],"version":4}},"aioseo_notices":[],"_links":{"self":[{"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/posts\/234"}],"collection":[{"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/users\/243"}],"replies":[{"embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/comments?post=234"}],"version-history":[{"count":3,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/posts\/234\/revisions"}],"predecessor-version":[{"id":238,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/posts\/234\/revisions\/238"}],"wp:attachment":[{"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/media?parent=234"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/categories?post=234"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/Tecnologiasdelainformacionparaelmundodelmanana\/wp-json\/wp\/v2\/tags?post=234"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}