Hi all, I've been trying to implement a lock-free stack here: https://github.com/vmchale/stack. Unfortunately, this is not something I'm particularly familiar with, and it segfaults around 70% of the time I try to actually do anything with it.
Here is the static bit:
%{#
#include <stdatomic.h>
%}
typedef aptr(l: addr) = $extype "_Atomic void**"
datavtype pointer_t(a: vt@ype) =
| pointer_t of node_t(a)
| none_t
and node_t(a: vt@ype) =
| node_t of @{ value = [ l : addr | l > null ] (a @ l | aptr(l))
, next = pointer_t(a)
}
vtypedef stack_t(a: vt@ype) = @{ stack_head = pointer_t(a) }
castfn release_stack {a:vt@ype} (stack_t(a)) : void
fun new {a:vt@ype} (&stack_t(a)? >> stack_t(a)) : void
fun {a:vt@ype} push (&stack_t(a) >> stack_t(a), a) : void
fun {a:vt@ype} pop (&stack_t(a) >> _) : Option_vt(a)
fun newm {a:vt@ype} () : stack_t(a)
fn atomic_store {a:vt@ype}{ l : addr | l > null }(a? @ l | aptr(l), a) :
(a @ l | void) =
"mac#"
fn atomic_load {a:vt@ype}{ l : addr | l > null }(a @ l | aptr(l)) : a =
"mac#"
fn leaky_malloc {a:vt@ype}{ sz : int | sz == sizeof(a) }(sz : size_t(sz)) :
[ l : addr | l > null ] (a? @ l | aptr(l)) =
"mac#malloc"
And here is the implementation:
staload "SATS/stack.sats"
implement new (st) =
st.stack_head := none_t
implement {a} push (st, x) =
let
val (pf_pre | ptr) = leaky_malloc(sizeof<a>)
val (pf | ()) = atomic_store(pf_pre | ptr, x)
val next_node = node_t(@{ value = (pf | ptr), next = st.stack_head })
val () = st.stack_head := pointer_t(next_node)
in end
implement {a} pop (st) =
case+ st.stack_head of
| ~pointer_t (~node_t (nd)) =>
begin
let
val (pf | aptr) = nd.value
val x = atomic_load(pf | aptr)
val () = st.stack_head := nd.next
in
Some_vt(x)
end
end
| none_t() => None_vt()
It's based on the Michael-Scott paper
http://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf, but I
worry about the frees in the pattern match (of ~node_t and ~pointer_t),
and in fact this does segfault when I try to use it for parallel
directory traversal.
Cheers,
Vanessa McHale
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/e1a19c62-5759-c930-4684-ffae2dec0813%40iohk.io.
signature.asc
Description: OpenPGP digital signature
