Skip to content

Commit

Permalink
Update kcas doc for main
Browse files Browse the repository at this point in the history
  • Loading branch information
polytypic committed Feb 15, 2024
1 parent 1eb56c4 commit a86f730
Show file tree
Hide file tree
Showing 27 changed files with 2,034 additions and 24 deletions.
4 changes: 3 additions & 1 deletion doc/kcas/Kcas/Loc/index.html

Large diffs are not rendered by default.

4 changes: 3 additions & 1 deletion doc/kcas/Kcas/Mode/index.html
Original file line number Diff line number Diff line change
@@ -1,2 +1,4 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Mode (kcas.Kcas.Mode)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../../index.html">kcas</a> &#x00BB; <a href="../index.html">Kcas</a> &#x00BB; Mode</nav><header class="odoc-preamble"><h1>Module <code><span>Kcas.Mode</span></code></h1><p>Operating modes of the <code>k-CAS-n-CMP</code> algorithm.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span><span>[ </span></code><ol><li id="type-t.Lock_free" class="def variant constructor anchored"><a href="#type-t.Lock_free" class="anchor"></a><code><span>| </span><span>`Lock_free</span></code><div class="def-doc"><span class="comment-delim">(*</span><p>In <code>`Lock_free</code> mode the algorithm makes sure that at least one domain will be able to make progress at the cost of performing read-only operations as read-write operations.</p><span class="comment-delim">*)</span></div></li><li id="type-t.Obstruction_free" class="def variant constructor anchored"><a href="#type-t.Obstruction_free" class="anchor"></a><code><span>| </span><span>`Obstruction_free</span></code><div class="def-doc"><span class="comment-delim">(*</span><p>In <code>`Obstruction_free</code> mode the algorithm proceeds optimistically and allows read-only operations to fail due to interference from other domains that might have been prevented in the <code>`Lock_free</code> mode.</p><span class="comment-delim">*)</span></div></li></ol><code><span> ]</span></code></div><div class="spec-doc"><p>Type of an operating mode of the <code>k-CAS-n-CMP</code> algorithm.</p></div></div></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Mode (kcas.Kcas.Mode)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script><script>let base_url = '../../../';
let search_urls = ['../../db.js','../../../sherlodoc.js'];
</script><script src="../../../odoc.support/odoc_search.js" defer="defer"></script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../../index.html">kcas</a> &#x00BB; <a href="../index.html">Kcas</a> &#x00BB; Mode</nav><div class="odoc-search"><div class="search-inner"><input class="search-bar" placeholder="🔎 Search..."/><div class="search-snake"></div><div class="search-result"></div></div></div><header class="odoc-preamble"><h1>Module <code><span>Kcas.Mode</span></code></h1><p>Operating modes of the <code>k-CAS-n-CMP</code> algorithm.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span><span> = </span><span>[ </span></code><ol><li id="type-t.Lock_free" class="def variant constructor anchored"><a href="#type-t.Lock_free" class="anchor"></a><code><span>| </span><span>`Lock_free</span></code><div class="def-doc"><span class="comment-delim">(*</span><p>In <code>`Lock_free</code> mode the algorithm makes sure that at least one domain will be able to make progress at the cost of performing read-only operations as read-write operations.</p><span class="comment-delim">*)</span></div></li><li id="type-t.Obstruction_free" class="def variant constructor anchored"><a href="#type-t.Obstruction_free" class="anchor"></a><code><span>| </span><span>`Obstruction_free</span></code><div class="def-doc"><span class="comment-delim">(*</span><p>In <code>`Obstruction_free</code> mode the algorithm proceeds optimistically and allows read-only operations to fail due to interference from other domains that might have been prevented in the <code>`Lock_free</code> mode.</p><span class="comment-delim">*)</span></div></li></ol><code><span> ]</span></code></div><div class="spec-doc"><p>Type of an operating mode of the <code>k-CAS-n-CMP</code> algorithm.</p></div></div></div></body></html>
4 changes: 3 additions & 1 deletion doc/kcas/Kcas/Retry/index.html
Original file line number Diff line number Diff line change
@@ -1,2 +1,4 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Retry (kcas.Kcas.Retry)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../../index.html">kcas</a> &#x00BB; <a href="../index.html">Kcas</a> &#x00BB; Retry</nav><header class="odoc-preamble"><h1>Module <code><span>Kcas.Retry</span></code></h1><p>Retry support.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec exception anchored" id="exception-Later"><a href="#exception-Later" class="anchor"></a><code><span><span class="keyword">exception</span> </span><span><span class="exception">Later</span></span></code></div><div class="spec-doc"><p>Exception that may be raised to signal that the operation, such as <a href="../Loc/index.html#val-get_as"><code>Loc.get_as</code></a>, <a href="../Loc/index.html#val-update"><code>Loc.update</code></a>, or <a href="../Xt/index.html#val-commit"><code>Xt.commit</code></a>, should be retried, at some point in the future, after the examined shared memory location or locations have changed.</p><p><b>NOTE</b>: It is important to understand that &quot;<i>after</i>&quot; may effectively mean &quot;<i>immediately</i>&quot;, because it may be the case that the examined shared memory locations have already changed.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-later"><a href="#val-later" class="anchor"></a><code><span><span class="keyword">val</span> later : <span>unit <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p><code>later ()</code> is equivalent to <code>raise Later</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-unless"><a href="#val-unless" class="anchor"></a><code><span><span class="keyword">val</span> unless : <span>bool <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>unless condition</code> is equivalent to <code>if not condition then later ()</code>.</p></div></div><div class="odoc-spec"><div class="spec exception anchored" id="exception-Invalid"><a href="#exception-Invalid" class="anchor"></a><code><span><span class="keyword">exception</span> </span><span><span class="exception">Invalid</span></span></code></div><div class="spec-doc"><p>Exception that may be raised to signal that the transaction log is no longer valid, e.g. because shared memory locations have been changed outside of the transaction, and the transaction should be retried.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-invalid"><a href="#val-invalid" class="anchor"></a><code><span><span class="keyword">val</span> invalid : <span>unit <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p><code>invalid ()</code> is equivalent to <code>raise Invalid</code>.</p></div></div></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Retry (kcas.Kcas.Retry)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script><script>let base_url = '../../../';
let search_urls = ['../../db.js','../../../sherlodoc.js'];
</script><script src="../../../odoc.support/odoc_search.js" defer="defer"></script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../../index.html">kcas</a> &#x00BB; <a href="../index.html">Kcas</a> &#x00BB; Retry</nav><div class="odoc-search"><div class="search-inner"><input class="search-bar" placeholder="🔎 Search..."/><div class="search-snake"></div><div class="search-result"></div></div></div><header class="odoc-preamble"><h1>Module <code><span>Kcas.Retry</span></code></h1><p>Retry support.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec exception anchored" id="exception-Later"><a href="#exception-Later" class="anchor"></a><code><span><span class="keyword">exception</span> </span><span><span class="exception">Later</span></span></code></div><div class="spec-doc"><p>Exception that may be raised to signal that the operation, such as <a href="../Loc/index.html#val-get_as"><code>Loc.get_as</code></a>, <a href="../Loc/index.html#val-update"><code>Loc.update</code></a>, or <a href="../Xt/index.html#val-commit"><code>Xt.commit</code></a>, should be retried, at some point in the future, after the examined shared memory location or locations have changed.</p><p><b>NOTE</b>: It is important to understand that &quot;<i>after</i>&quot; may effectively mean &quot;<i>immediately</i>&quot;, because it may be the case that the examined shared memory locations have already changed.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-later"><a href="#val-later" class="anchor"></a><code><span><span class="keyword">val</span> later : <span>unit <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p><code>later ()</code> is equivalent to <code>raise Later</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-unless"><a href="#val-unless" class="anchor"></a><code><span><span class="keyword">val</span> unless : <span>bool <span class="arrow">&#45;&gt;</span></span> unit</span></code></div><div class="spec-doc"><p><code>unless condition</code> is equivalent to <code>if not condition then later ()</code>.</p></div></div><div class="odoc-spec"><div class="spec exception anchored" id="exception-Invalid"><a href="#exception-Invalid" class="anchor"></a><code><span><span class="keyword">exception</span> </span><span><span class="exception">Invalid</span></span></code></div><div class="spec-doc"><p>Exception that may be raised to signal that the transaction log is no longer valid, e.g. because shared memory locations have been changed outside of the transaction, and the transaction should be retried.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-invalid"><a href="#val-invalid" class="anchor"></a><code><span><span class="keyword">val</span> invalid : <span>unit <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span></span></code></div><div class="spec-doc"><p><code>invalid ()</code> is equivalent to <code>raise Invalid</code>.</p></div></div></div></body></html>
4 changes: 3 additions & 1 deletion doc/kcas/Kcas/Timeout/index.html
Original file line number Diff line number Diff line change
@@ -1,2 +1,4 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Timeout (kcas.Kcas.Timeout)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../../index.html">kcas</a> &#x00BB; <a href="../index.html">Kcas</a> &#x00BB; Timeout</nav><header class="odoc-preamble"><h1>Module <code><span>Kcas.Timeout</span></code></h1><p>Timeout support.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec exception anchored" id="exception-Timeout"><a href="#exception-Timeout" class="anchor"></a><code><span><span class="keyword">exception</span> </span><span><span class="exception">Timeout</span></span></code></div><div class="spec-doc"><p>Exception that may be raised by operations such as <a href="../Loc/index.html#val-get_as"><code>Loc.get_as</code></a>, <a href="../Loc/index.html#val-update"><code>Loc.update</code></a>, <a href="../Loc/index.html#val-modify"><code>Loc.modify</code></a>, or <a href="../Xt/index.html#val-commit"><code>Xt.commit</code></a> when given a <code>~timeoutf</code> in seconds.</p></div></div></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Timeout (kcas.Kcas.Timeout)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script><script>let base_url = '../../../';
let search_urls = ['../../db.js','../../../sherlodoc.js'];
</script><script src="../../../odoc.support/odoc_search.js" defer="defer"></script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../../index.html">kcas</a> &#x00BB; <a href="../index.html">Kcas</a> &#x00BB; Timeout</nav><div class="odoc-search"><div class="search-inner"><input class="search-bar" placeholder="🔎 Search..."/><div class="search-snake"></div><div class="search-result"></div></div></div><header class="odoc-preamble"><h1>Module <code><span>Kcas.Timeout</span></code></h1><p>Timeout support.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec exception anchored" id="exception-Timeout"><a href="#exception-Timeout" class="anchor"></a><code><span><span class="keyword">exception</span> </span><span><span class="exception">Timeout</span></span></code></div><div class="spec-doc"><p>Exception that may be raised by operations such as <a href="../Loc/index.html#val-get_as"><code>Loc.get_as</code></a>, <a href="../Loc/index.html#val-update"><code>Loc.update</code></a>, <a href="../Loc/index.html#val-modify"><code>Loc.modify</code></a>, or <a href="../Xt/index.html#val-commit"><code>Xt.commit</code></a> when given a <code>~timeoutf</code> in seconds.</p></div></div></div></body></html>
4 changes: 3 additions & 1 deletion doc/kcas/Kcas/Xt/index.html
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Xt (kcas.Kcas.Xt)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../../index.html">kcas</a> &#x00BB; <a href="../index.html">Kcas</a> &#x00BB; Xt</nav><header class="odoc-preamble"><h1>Module <code><span>Kcas.Xt</span></code></h1><p>Explicit transaction log passing on shared memory locations.</p><p>This module provides a way to implement composable transactions over shared memory locations. A transaction is a function written by the library user and can be thought of as a specification of a sequence of <a href="#val-get"><code>Xt.get</code></a> and <a href="#val-set"><code>Xt.set</code></a> accesses to shared memory locations. To actually perform the accesses one then <a href="#val-commit"><code>Xt.commit</code></a>s the transaction.</p><p>Transactions should generally not perform arbitrary side-effects, because when a transaction is committed it may be attempted multiple times meaning that the side-effects are also performed multiple times. <a href="#val-post_commit"><code>Xt.post_commit</code></a> can be used to perform an action only once after the transaction has been committed succesfully.</p><p><b>WARNING</b>: To make it clear, the operations provided by the <a href="../Loc/index.html"><code>Loc</code></a> module for accessing individual shared memory locations do not implicitly go through the transaction mechanism and should generally not be used within transactions. There are advanced algorithms where one might, within a transaction, perform operations that do not get recorded into the transaction log. Using such techniques correctly requires expert knowledge and is not recommended for casual users.</p><p>As an example, consider an implementation of doubly-linked circular lists. Instead of using a mutable field, <code>ref</code>, or <code>Atomic.t</code>, one would use a shared memory location, or <a href="../Loc/index.html#type-t"><code>Loc.t</code></a>, for the pointers in the node type:</p><pre class="language-ocaml"><code>type 'a node = {
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Xt (kcas.Kcas.Xt)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script><script>let base_url = '../../../';
let search_urls = ['../../db.js','../../../sherlodoc.js'];
</script><script src="../../../odoc.support/odoc_search.js" defer="defer"></script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../../index.html">kcas</a> &#x00BB; <a href="../index.html">Kcas</a> &#x00BB; Xt</nav><div class="odoc-search"><div class="search-inner"><input class="search-bar" placeholder="🔎 Search..."/><div class="search-snake"></div><div class="search-result"></div></div></div><header class="odoc-preamble"><h1>Module <code><span>Kcas.Xt</span></code></h1><p>Explicit transaction log passing on shared memory locations.</p><p>This module provides a way to implement composable transactions over shared memory locations. A transaction is a function written by the library user and can be thought of as a specification of a sequence of <a href="#val-get"><code>Xt.get</code></a> and <a href="#val-set"><code>Xt.set</code></a> accesses to shared memory locations. To actually perform the accesses one then <a href="#val-commit"><code>Xt.commit</code></a>s the transaction.</p><p>Transactions should generally not perform arbitrary side-effects, because when a transaction is committed it may be attempted multiple times meaning that the side-effects are also performed multiple times. <a href="#val-post_commit"><code>Xt.post_commit</code></a> can be used to perform an action only once after the transaction has been committed succesfully.</p><p><b>WARNING</b>: To make it clear, the operations provided by the <a href="../Loc/index.html"><code>Loc</code></a> module for accessing individual shared memory locations do not implicitly go through the transaction mechanism and should generally not be used within transactions. There are advanced algorithms where one might, within a transaction, perform operations that do not get recorded into the transaction log. Using such techniques correctly requires expert knowledge and is not recommended for casual users.</p><p>As an example, consider an implementation of doubly-linked circular lists. Instead of using a mutable field, <code>ref</code>, or <code>Atomic.t</code>, one would use a shared memory location, or <a href="../Loc/index.html#type-t"><code>Loc.t</code></a>, for the pointers in the node type:</p><pre class="language-ocaml"><code>type 'a node = {
succ: 'a node Loc.t;
pred: 'a node Loc.t;
datum: 'a;
Expand Down
Loading

0 comments on commit a86f730

Please sign in to comment.