To share a global variable among threads without using a lock, one probably needs to introduce "special" views. For example, if a thread takes out a linear stack from the global vairable 'theStack', it cannot free it because it does not own the stack. I would think that linear views can help you reason
When doing a lock-free implementation, please make sure that you do not modify the content obtained from reading a shared global variable except via a call to compare-and-swap. On Sat, Mar 2, 2019 at 8:23 AM Vanessa McHale <[email protected]> wrote: > 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. 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/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 > > [image: Input Output] <http://iohk.io> > > [image: Twitter] <https://twitter.com/InputOutputHK> [image: Github] > <https://github.com/input-output-hk> [image: 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 [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/b8107961-a4b5-5222-ac08-6d85f885643f%40iohk.io > <https://groups.google.com/d/msgid/ats-lang-users/b8107961-a4b5-5222-ac08-6d85f885643f%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/CAPPSPLo5QYUOPTQ-fJYfXzNEwhPxNQmsQcVFKVDjBm7e0OMLpw%40mail.gmail.com.
