Thanks! Is there any neat way to use views with a lock-free stack, then? I'm fine ignoring frees for the moment, but it would be interesting to see how to do such a thing safely in ATS...
Cheers, Vanessa On 3/1/19 11:23 PM, gmhwxi wrote: > > If we ignore malloc/free, then lock-free stack implementation > should look more or less like the following code: > > > fun > pop(theStack) = let > var xs0 = theStack > in > case+ xs0 of > | nil() => None_vt() > | cons(x0, xs1) => > if atomic_compare_exchange(theStack, xs0, xs1) > then Some_vt(x0) else pop(theStack) > end > > fun > push(theStack, x0) = let > var xs0 = theStack > val xs1 = cons(x0, xs0) > in > if atomic_compare_exchange(theStack, xs0, xs1) then () else > push(theStack, x0) > end > > On Friday, March 1, 2019 at 11:05:44 PM UTC-5, gmhwxi wrote: > > 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 <vanessa...> wrote: > > Hi all, > > I've been trying to implement a lock-free stack here: > https://github.com/vmchale/stack > <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 > <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 > <mailto:ats-lang-users+unsubscr...@googlegroups.com>. > To post to this group, send email to > ats-lang-users@googlegroups.com > <mailto:ats-lang-users@googlegroups.com>. > Visit this group at > https://groups.google.com/group/ats-lang-users > <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 ats-lang-users+unsubscr...@googlegroups.com > <mailto:ats-lang-users+unsubscr...@googlegroups.com>. > To post to this group, send email to ats-lang-users@googlegroups.com > <mailto: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/d71163fe-91da-40c4-b68d-d605704a9db0%40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/d71163fe-91da-40c4-b68d-d605704a9db0%40googlegroups.com?utm_medium=email&utm_source=footer>. -- *Vanessa McHale* Functional Compiler Engineer | Chicago, IL Website: www.iohk.io <http://iohk.io> Twitter: @vamchale PGP Key ID: 4209B7B5 Input Output <http://iohk.io> Twitter <https://twitter.com/InputOutputHK> Github <https://github.com/input-output-hk> LinkedIn <https://www.linkedin.com/company/input-output-global> This e-mail and any file transmitted with it are confidential and intended solely for the use of the recipient(s) to whom it is addressed. Dissemination, distribution, and/or copying of the transmission by anyone other than the intended recipient(s) is prohibited. If you have received this transmission in error please notify IOHK immediately and delete it from your system. E-mail transmissions cannot be guaranteed to be secure or error free. We do not accept liability for any loss, damage, or error arising from this transmission -- 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/b8107961-a4b5-5222-ac08-6d85f885643f%40iohk.io.
signature.asc
Description: OpenPGP digital signature
