I looked around this morning to see what approaches are used nowadays for implementing lock-free data structures. It seems that RCU is the way to go: http://libcds.sourceforge.net/
With linear views, one should be able to capture some of the reasoning behind RCUs, facilitating the construction of lock-free data structures. Sounds like interesting stuff, but I must focus on implementing ATS3 for now :) On Sat, Mar 2, 2019 at 10:35 AM Hongwei Xi <[email protected]> wrote: > 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/CAPPSPLo1qOO3MNao_rEL5YCacHvf-yoDsmZNcpOzquEUswu4fQ%40mail.gmail.com.
