{"id":170167,"date":"2008-12-23T10:41:46","date_gmt":"2008-12-23T10:41:46","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/chalice\/"},"modified":"2017-06-05T12:34:23","modified_gmt":"2017-06-05T19:34:23","slug":"chalice","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/chalice\/","title":{"rendered":"Chalice"},"content":{"rendered":"<p><img loading=\"lazy\" decoding=\"async\" class=\"size-full wp-image-341903 alignleft\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/Chalice-logo.png\" alt=\"chalice-logo\" width=\"200\" height=\"170\" \/>Chalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. The language allows fine-grained locking via specifications that track fractional permissions for memory locations. The research project also includes an automatic static program verifier for Chalice.<\/p>\n<p>Because of its permissions model, Chalice has also been used as a test bed for <em>stepwise refinement<\/em>.\u00a0 Using refinement, one can write an abstract program (call it <em>pseudo-code<\/em>) and then provide a more concrete implementation for that pseudo-code.\u00a0 The pseudo-code and its refinements all become part of the program text, and the Chalice verifier checks the correctness of the refinement steps.\u00a0 An episode of <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/the-verification-corner\/\" target=\"_self\">Verification Corner<\/a> shows how this is done.<\/p>\n<p>Chalice is available for <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/boogie.codeplex.com\/\" target=\"_blank\">download<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> as open source from the Boogie open-source repository.\u00a0 There is also a <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/boogie.codeplex.com\/releases\/view\/72005\">nightly build<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> that contains the binaries, available from &#8220;planned&#8221; releases on the Download tab.<\/p>\n<h2>Learn more<\/h2>\n<p>If you want to program in Chalice or learn how its specifications are used (or, for that matter, to learn the basics of what makes a concurrent program correct), the Chalice tutorial is for you.<\/p>\n<ul>\n<li>Try <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" title=\"\" href=\"http:\/\/rise4fun.com\/\" target=\"_blank\">Chalice in your browser<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>!<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/boogie.codeplex.com\/releases\/view\/72005\">Download<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> Chalice<\/li>\n<li>Contribute to the Chalice <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/boogie.codeplex.com\/\">source development<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Read the <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/krml197.pdf\">Chalice tutorial<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Chalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. The language allows fine-grained locking via specifications that track fractional permissions for memory locations. The research project also includes [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170167","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2008-12-23","related-publications":[342062,342077,342974,343076,343088,343118,345044,345050,345524],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170167","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":0,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170167\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170167"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170167"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170167"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170167"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170167"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}