I took a quick look. The paper gives an algorithm for implementing a queue, and your code implements a stack. The stack implementation contains a few race conditions. For example, say that thread A pops and thread B pops as well; after thread A frees a node, thread B could try to free it again, resulting in a very common crash caused by "double-free".
On Thu, Feb 28, 2019 at 12:10 PM Vanessa McHale <[email protected]> wrote: > 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 [email protected]. > To post to this group, send email to [email protected]. > 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 > <https://groups.google.com/d/msgid/ats-lang-users/e1a19c62-5759-c930-4684-ffae2dec0813%40iohk.io?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To post to this group, send email to [email protected]. 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/CAPPSPLp7Lqi5TT_3FtGmuR8%3DdLmhMq5%3D1a_R4tOZSrwruyiw7g%40mail.gmail.com.
