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 [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/159f0461-8890-4dfe-9490-c31bb322d859%40googlegroups.com.
