A Mechanically Verified Garbage Collector for OCaml

A Mechanically Verified Garbage Collector for OCaml | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article A Mechanically Verified Garbage Collector for OCaml Sheera Shamsu, Dipesh Kaphle, Dhruv Maroo, Kartik Nagar, Karthikeyan Bhargavan, and 1 more This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-4674167/v1 This work is licensed under a CC BY 4.0 License Status: Published Journal Publication published 14 May, 2025 Read the published version in Journal of Automated Reasoning → Version 1 posted 11 You are reading this latest preprint version Abstract The OCaml programming language finds application across diverse domains, including systems programming, web development, scientific computing, formal verification, and symbolic mathematics. OCaml is a memory-safe programming language that uses a garbage collector (GC) to free unreachable memory. OCaml features a low-latency, high-performance GC, turned for functional programming. The GC has two generations -- a minor heap collected using a copying collector and a major heap collected using an incremental mark-and-sweep collector. Alongside the intricacies of an efficient GC design, OCaml compiler uses efficient object representations for some object classes, such as interior pointers for supporting mutually recursive functions, which further complicates the GC design. The GC is a critical component of the OCaml runtime system, and its correctness is essential for the safety of OCaml programs. In this paper, we propose a strategy for crafting a correct, proof-oriented GC from scratch, designed to evolve over time with additional language features. Our approach neatly separates abstract GC correctness from OCaml-specific GC correctness, offering the ability to integrate further GC optimizations, while preserving core abstract GC correctness. As an initial step to demonstrate the viability of our approach, we have developed a verified stop-the-world mark-and-sweep GC for OCaml. The approach is fully mechanized in F* and its low-level subset Low*. We use the KaRaMel compiler to compile Low* to C, and integrate the verified GC with the OCaml runtime. Our GC is evaluated against off-the-shelf OCaml GC and Boehm-Demers-Weiser conservative GC, and the experimental results show that verified OCaml GC is competitive with the standard OCaml GC. formal verification mark and sweep garbage collection F* Low* mechanized formal proofs graph traversal proofs Full Text Additional Declarations No competing interests reported. Supplementary Files JARLATEXsourceSuppl.zip Cite Share Download PDF Status: Published Journal Publication published 14 May, 2025 Read the published version in Journal of Automated Reasoning → Version 1 posted Editorial decision: Revision requested 21 Oct, 2024 Reviews received at journal 21 Oct, 2024 Reviews received at journal 04 Oct, 2024 Reviews received at journal 29 Sep, 2024 Reviewers agreed at journal 08 Jul, 2024 Reviewers agreed at journal 05 Jul, 2024 Reviewers agreed at journal 03 Jul, 2024 Reviewers invited by journal 03 Jul, 2024 Editor assigned by journal 02 Jul, 2024 Submission checks completed at journal 02 Jul, 2024 First submitted to journal 02 Jul, 2024 You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-4674167","acceptedTermsAndConditions":true,"allowDirectSubmit":false,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":324207702,"identity":"17a076dc-efc5-46db-87d8-4b86c18c5dda","order_by":0,"name":"Sheera Shamsu","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAAA6ElEQVRIiWNgGAWjYDACCShtwMDA+ABI8/CRooXZAKSFjRQtbGA2QS3ys5sPPq6oYbA3Fzv+rPJrjp0MGwPzw0c38GgxuHMs2fDMMYbEnbNzzG7LbksGOozN2DgHnxaJHDPJBjaGBIPbOWy3JbcxA7XwsEnj0yI/I//7z4Z/DPYGt9OfFUtuqyesheFGDhtjYxsD44bbCWaMH7cdJqzF4EaasWRjn0Tihts5xtKM247zsDET8Iv8jOSHHxu+2YAc9vDjz23V9vzszQ8f43UYBEBih5kHTBJWjgCMP0hRPQpGwSgYBSMGAAD1LEO08TbC2AAAAABJRU5ErkJggg==","orcid":"","institution":"Indian Institute of Technology Madras","correspondingAuthor":true,"prefix":"","firstName":"Sheera","middleName":"","lastName":"Shamsu","suffix":""},{"id":324207703,"identity":"ba105ffb-b453-4979-9aeb-0102a1e99ff5","order_by":1,"name":"Dipesh Kaphle","email":"","orcid":"","institution":"National Institute of Technology Tiruchirappalli","correspondingAuthor":false,"prefix":"","firstName":"Dipesh","middleName":"","lastName":"Kaphle","suffix":""},{"id":324207704,"identity":"bd56a21b-e4ba-4ad3-ab8c-c5d853447231","order_by":2,"name":"Dhruv Maroo","email":"","orcid":"","institution":"Indian Institute of Technology Madras","correspondingAuthor":false,"prefix":"","firstName":"Dhruv","middleName":"","lastName":"Maroo","suffix":""},{"id":324207705,"identity":"9eacf3bf-1113-4b48-a048-9bb958316f7e","order_by":3,"name":"Kartik Nagar","email":"","orcid":"","institution":"Indian Institute of Technology Madras","correspondingAuthor":false,"prefix":"","firstName":"Kartik","middleName":"","lastName":"Nagar","suffix":""},{"id":324207706,"identity":"da2b2130-397f-4ef4-aaaa-a842c16ab57b","order_by":4,"name":"Karthikeyan Bhargavan","email":"","orcid":"","institution":"INRIA, Paris","correspondingAuthor":false,"prefix":"","firstName":"Karthikeyan","middleName":"","lastName":"Bhargavan","suffix":""},{"id":324207707,"identity":"d0a30588-37b5-4e28-8255-e02b953f69c6","order_by":5,"name":"Sivaramakrishnan KC","email":"","orcid":"","institution":"Indian Institute of Technology Madras","correspondingAuthor":false,"prefix":"","firstName":"Sivaramakrishnan","middleName":"","lastName":"KC","suffix":""}],"badges":[],"createdAt":"2024-07-02 12:21:14","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-4674167/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-4674167/v1","draftVersion":[],"editorialEvents":[{"content":"https://doi.org/10.1007/s10817-025-09721-0","type":"published","date":"2025-05-14T15:57:28+00:00"}],"editorialNote":"","failedWorkflow":false,"files":[{"id":83068045,"identity":"5313f322-cb25-43d8-a730-5b3a4e355dc2","added_by":"auto","created_at":"2025-05-19 16:09:42","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":769177,"visible":true,"origin":"","legend":"","description":"","filename":"snarticle.pdf","url":"https://assets-eu.researchsquare.com/files/rs-4674167/v1_covered_81602f58-d12d-481a-81ab-f50881bf802f.pdf"},{"id":61031469,"identity":"5975a261-fb7f-49e4-afca-391fb3f6917e","added_by":"auto","created_at":"2024-07-24 19:39:24","extension":"zip","order_by":2,"title":"","display":"","copyAsset":false,"role":"supplement","size":43555160,"visible":true,"origin":"","legend":"","description":"","filename":"JARLATEXsourceSuppl.zip","url":"https://assets-eu.researchsquare.com/files/rs-4674167/v1/40b31974d93f7b67e0b4f2a0.zip"}],"financialInterests":"No competing interests reported.","formattedTitle":"A Mechanically Verified Garbage Collector for OCaml","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":false,"highlight":"","institution":"","isAcceptedByJournal":true,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":true,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"journal-of-automated-reasoning","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"jars","sideBox":"Learn more about [Journal of Automated Reasoning](http://link.springer.com/journal/10817)","snPcode":"10817","submissionUrl":"https://submission.nature.com/new-submission/10817/3","title":"Journal of Automated Reasoning","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"em","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false},"keywords":"formal verification, mark and sweep garbage collection, F*, Low*, mechanized formal proofs, graph traversal proofs","lastPublishedDoi":"10.21203/rs.3.rs-4674167/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-4674167/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"\u003cp\u003eThe OCaml programming language finds application across diverse domains, including systems programming, web development, scientific computing, formal verification, and symbolic mathematics. OCaml is a memory-safe programming language that uses a garbage collector (GC) to free unreachable memory. OCaml features a low-latency, high-performance GC, turned for functional programming. The GC has two generations -- a minor heap collected using a copying collector and a major heap collected using an incremental mark-and-sweep collector. Alongside the intricacies of an efficient GC design, OCaml compiler uses efficient object representations for some object classes, such as interior pointers for supporting mutually recursive functions, which further complicates the GC design. The GC is a critical component of the OCaml runtime system, and its correctness is essential for the safety of OCaml programs.\u0026nbsp;\u003c/p\u003e\n\u003cp\u003eIn this paper, we propose a strategy for crafting a correct, proof-oriented GC from scratch, designed to evolve over time with additional language features. Our approach neatly separates abstract GC correctness from OCaml-specific GC correctness, offering the ability to integrate further GC optimizations, while preserving core abstract GC correctness. As an initial step to demonstrate the viability of our approach, we have developed a verified stop-the-world mark-and-sweep GC for OCaml. The approach is fully mechanized in F* and its low-level subset Low*. We use the KaRaMel compiler to compile Low* to C, and integrate the verified GC with the OCaml runtime. Our GC is evaluated against off-the-shelf OCaml GC and Boehm-Demers-Weiser conservative GC, and the experimental results show that verified OCaml GC is competitive with the standard OCaml GC.\u003c/p\u003e","manuscriptTitle":"A Mechanically Verified Garbage Collector for OCaml","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2024-07-24 19:39:19","doi":"10.21203/rs.3.rs-4674167/v1","editorialEvents":[{"type":"communityComments","content":0},{"type":"decision","content":"Revision requested","date":"2024-10-21T12:19:39+00:00","index":"","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2024-10-21T11:46:52+00:00","index":"hide","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2024-10-04T10:18:57+00:00","index":"hide","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2024-09-29T21:53:24+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"212065281796020530062548573425823943480","date":"2024-07-08T13:47:26+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"197758463681948586737025561347383342683","date":"2024-07-05T10:23:29+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"64132937789691200729244427064141718716","date":"2024-07-03T10:20:31+00:00","index":"hide","fulltext":""},{"type":"reviewersInvited","content":"","date":"2024-07-03T10:16:10+00:00","index":"","fulltext":""},{"type":"editorAssigned","content":"","date":"2024-07-02T13:39:18+00:00","index":"","fulltext":""},{"type":"checksComplete","content":"","date":"2024-07-02T13:38:53+00:00","index":"","fulltext":""},{"type":"submitted","content":"Journal of Automated Reasoning","date":"2024-07-02T12:19:17+00:00","index":"","fulltext":""}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"journal-of-automated-reasoning","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"jars","sideBox":"Learn more about [Journal of Automated Reasoning](http://link.springer.com/journal/10817)","snPcode":"10817","submissionUrl":"https://submission.nature.com/new-submission/10817/3","title":"Journal of Automated Reasoning","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"em","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false}}],"origin":"","ownerIdentity":"26b0b791-e821-4dfd-8cc0-c8dd929bd4b0","owner":[],"postedDate":"July 24th, 2024","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"published-in-journal","subjectAreas":[],"tags":[],"updatedAt":"2025-05-19T16:06:11+00:00","versionOfRecord":{"articleIdentity":"rs-4674167","link":"https://doi.org/10.1007/s10817-025-09721-0","journal":{"identity":"journal-of-automated-reasoning","isVorOnly":false,"title":"Journal of Automated Reasoning"},"publishedOn":"2025-05-14 15:57:28","publishedOnDateReadable":"May 14th, 2025"},"versionCreatedAt":"2024-07-24 19:39:19","video":"","vorDoi":"10.1007/s10817-025-09721-0","vorDoiUrl":"https://doi.org/10.1007/s10817-025-09721-0","workflowStages":[]},"version":"v1","identity":"rs-4674167","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-4674167","identity":"rs-4674167","version":["v1"]},"buildId":"qtupq5eGEP_6zYnWcrvyt","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}