I don't think it's due to polymorphic functions, because the problem goes away when I switch to using only one thread.
Cheers, Vanessa On 3/1/19 8:43 PM, Richard wrote: > At first glance, making the functions polymorphic (as opposed to templates) > could be a potential reason for segmentation faults (see > https://github.com/githwxi/ATS-Postiats/issues/216). Though mixing dependent > types and templates together has also been known to cause issues (see > https://groups.google.com/d/msgid/ats-lang-users/c7885759-c97b-482e-a9a8-313152cc1e6b%40googlegroups.com?utm_medium=email&utm_source=footer) > > On Thursday, February 28, 2019 at 12:10:50 PM UTC-5, Vanessa McHale 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 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/f4cf974c-6486-0064-d12d-292694bdf4a4%40iohk.io.
signature.asc
Description: OpenPGP digital signature
