{"id":4746,"date":"2015-01-28T07:56:28","date_gmt":"2015-01-28T06:56:28","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4746"},"modified":"2015-01-28T07:56:28","modified_gmt":"2015-01-28T06:56:28","slug":"resena-mutual-exclusion-by-four-shared-bits-with-not-more-than-quadratic-complexity","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-mutual-exclusion-by-four-shared-bits-with-not-more-than-quadratic-complexity\/","title":{"rendered":"Rese\u00f1a: Mutual exclusion by four shared bits with not more than quadratic complexity"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/pvs.csl.sri.com\">PVS<\/a> sobre concurrencia titulado <a href=\"http:\/\/wimhesselink.nl\/mechver\/mx4bits\/whh483.pdf\">Mutual exclusion by four shared bits with not more than quadratic complexity<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/wimhesselink.nl\">Wim H. Hesselink<\/a> (de la Universidad de Groninga, Pa\u00edses Bajos).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  For years, the mutual exclusion algorithm of Lycklama and Hadzilacos (1991) was the optimal mutual exclusion algorithm with the first-come-first-served property, with a minimal number of (non-atomic) communication variables (5 bits per thread). Recently, Aravind published an improvement of it, which uses 4 bits per threads and has simplified waiting conditions. This algorithm is extended here with fault tolerance, and it is verified by assertional methods, using the proof assistant PVS. Progress is proved by means of UNITY logic. The paper proposes a new measure of concurrent time complexity, and proves that the concurrent complexity for throughput of the present algorithm is not more than quadratic in the number of threads.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en PVS se encuentra <a href=\"http:\/\/wimhesselink.nl\/mechver\/mx4bits\/dumpMx4bitLHA201409.gz\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en PVS sobre concurrencia titulado Mutual exclusion by four shared bits with not more than quadratic complexity. Su autor es Wim H. Hesselink (de la Universidad de Groninga, Pa\u00edses Bajos). Su resumen es For years, the mutual exclusion algorithm of Lycklama and Hadzilacos (1991) was the optimal&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[277,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4746"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4746"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4746\/revisions"}],"predecessor-version":[{"id":4747,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4746\/revisions\/4747"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4746"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4746"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4746"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}