Data race? Or something else going wrong?

231 Views Asked by At

Found the programming language "pony" just today... and started to play with it.

My code is supposed to do some simple producer consumer thing. As claimed by language documentation, the language ensures there are no data races.

Here, main sends 10 messages to the producer, which in turn sends 10 messages to the consumer. The consumer increments a counter state variable. Then, main sends a message to the consumer, which in turn sends a message to main in order to display the current value. If all messages were in sequence, the expected value would be 9 (or 10). The result printed, though is 0.

As this is all in hour 1 of my playing with the language, of course I might have messed up something else.

Who can explain my mistake?

use "collections"

actor Consumer 
    var _received : I32
    new create() =>
        _received = 0
    be tick() =>
        _received = _received + 1
    be query(main : Main) =>
        main.status(_received)

actor Producer
    var _consumer : Consumer
    new create(consumer' : Consumer) =>
        _consumer = consumer'

    be produceOne () =>
        _consumer.tick()

actor Main
    var _env : Env 
    new create(env: Env) =>
        _env = env
        let c : Consumer = Consumer.create()
        let p = Producer.create(c)
        for i in Range[I32](0,10) do
            p.produceOne()
        end
        c.query(this)

    be status( count : I32) =>
        // let fortyTwo : I32 = 42
        // _env.out.print( "fortytwo? " + (fortyTwo.string()))
        _env.out.print( "produced: " + (count.string()) )

Running on windows 10, 64 bit, btw. with the latest and greatest zip file installation I found.

0.10.0-1c33065 [release] compiled with: llvm 3.9.0 -- ?

2

There are 2 best solutions below

1
Benoit Vey On BEST ANSWER

The data races prevented by Pony are the ones that occur at the memory level, when somebody reads from a memory location while somebody else is writing to it. This is prevented by forbidding shared mutable state with the type system.

However, your program can still have "logical" data races if a result depends on a message ordering that isn't guaranteed by Pony. Pony guarantees causal ordering of messages. This means that message sent or received is the cause of any future message that will be sent or received if the messages have the same destination, and of course causes must happen before their effects.

actor A
  be ma(b: B, c: C) =>
    b.mb()
    c.mc(b)

actor B
  be mb() =>
    None

actor C
  be mc(b: B) =>
    b.mb()

In this example, B will always receive the message from A before the message from C because A sends a message to B before sending a message to C (note that the two messages can still be received in any order since they don't have the same destination). This means that the message sent to B by C is sent after the message sent to B by A and since both have the same destination, there is a causal relationship.

Let's look at the causal orderings in your program. With -> being "is the cause of", we have

  • Main.create -> Main.status (through Consumer.query)
  • Consumer.create -> Consumer.query
  • Consumer.create -> Consumer.tick (through Producer.produceOne)
  • Producer.create -> Producer.produceOne

As you can see, there is no causal relationship between Consumer.query and Consumer.tick. In the sense of the actual implementation, this means that Main can send the produceOne messages and then send the query message before any Producer starts executing the message it received and has a chance to send the tick message. If you run your program with one scheduler thread (--ponythreads=1 as a command line argument) it will always print produced: 0 because Main will monopolise the only scheduler until the end of create. With multiple scheduler threads, anything between 0 and 10 can happen because all schedulers could be busy executing other actors, or be available to start executing the Producers immediately.

In summary, your tick and query behaviours can be executed in any particular order. To fix the problem, you'd have to introduce causality between your messages, either by adding round-trip messages or by doing the accumulating and printing in the same actor.

0
BitTickler On

Thanks to @Benoit Vey for the help with that.

It is indeed the case, that there is no express or implied casuality between the execution of the query and the time when the producer executes its tick () messaging to the consumer.

In that sense, no voodoo, no magic. It all just behaves as any actor system would be expected to behave.

Messages within an actor are processed in order (as it should be). Hence, in order to get the desired program behavior, the producer should trigger the query eventually (in order after processing the produceOne messages).

Here, how that can be accomplished:

use "collections"

actor Consumer 
    var _received : I32
    new create() =>
        _received = 0
    be tick() =>
        _received = _received + 1
    be query(main : Main) =>
        main.status(_received)

actor Producer
    var _consumer : Consumer
    new create(consumer' : Consumer) =>
        _consumer = consumer'

    be produceOne () =>
        _consumer.tick()

    be forward (main : Main) =>
        main.doQuery(_consumer)

actor Main
    var _env : Env 
    new create(env: Env) =>
        _env = env
        let c : Consumer = Consumer.create()
        let p = Producer.create(c)
        for i in Range[I32](0,10) do
            p.produceOne()
        end
        //c.query(this)
        p.forward(this)

    be doQuery (target : Consumer) =>
        target.query(this)

    be status( count : I32) =>
        // let fortyTwo : I32 = 42
        // _env.out.print( "fortytwo? " + (fortyTwo.string()))
        _env.out.print( "produced: " + (count.string()) )

Just for giggles (and comparison), I also implemented the same in F#. And to my surprise, pony wins in the category of compactness. 39 lines of code in Pony, 80 lines in F#. That, along with the native code generation makes Pony an interesting language choice indeed.

open FSharp.Control

type ConsumerMessage =
    | Tick
    | Query of MailboxProcessor<MainMessage>

and ProducerMessage =
    | ProduceOne of MailboxProcessor<ConsumerMessage>
    | Forward of (MailboxProcessor<MainMessage> * MainMessage)

and MainMessage =
    | Status of int
    | DoQuery of MailboxProcessor<ConsumerMessage>

let consumer = 
    new MailboxProcessor<ConsumerMessage>
        (fun inbox ->
            let rec loop count =
                async {
                    let! m = inbox.Receive()
                    match m with
                    | Tick ->
                        return! loop (count+1)
                    | Query(target) ->
                        do target.Post(Status count)
                        return! loop count
                }        
            loop 0
        )

let producer =
    new MailboxProcessor<ProducerMessage>
        (fun inbox ->
            let rec loop () =
                async {
                    let! m = inbox.Receive()
                    match m with
                    | ProduceOne(consumer') ->
                        consumer'.Post(Tick)
                        return! loop ()
                    | Forward (target, msg) ->
                        target.Post(msg)
                        return! loop ()
                }
            loop ()
        )

let main =
    new MailboxProcessor<MainMessage>
        (fun inbox ->
            let rec loop () =
                async {
                    let! m = inbox.Receive()
                    match m with
                    | Status(count) ->
                        printfn "Status: %d" count
                        return! loop ()
                    | DoQuery(target) ->
                        target.Post(Query inbox)
                        return! loop ()
                }
            loop ()
        )

let init() =
    main.Start()
    consumer.Start()
    producer.Start()

let run() =
    for _ in [1..10] do
        producer.Post(ProduceOne consumer)
    producer.Post(Forward(main,DoQuery consumer))

let query () = 
    consumer.Post(Query main)

let go() =
    init ()
    run ()
    //query ()