[erlang-questions] help with smoker's problem

[Matthias Lang]

On Tuesday, August 19, Ulises wrote:
> I know this is not a CS list however I'll dare and post my solution to
> the smokers problem in Erlang. Could anybody tell me if it's correct?

It looks correct to me*, though you can probably argue forever over
whether the two conditions are met or not.

Two comments:

  - If you spawn like this: spawn(fun() -> smoker(tobacco) end)
    then you don't need to export smoker/1 and thus probably
    don't need to use export_all. Opinions differ over whether
    export_all is "usually bad" or not, but most people 
    agree that spawning via funs is a good idea.

  - Registering processes is something I do sparingly. I would have
    started the arbiter with a list of smoker PIDs instead of 
    registering the smokers. 

  - Telling the smokers what they're supplying but then not using
    that atom is suspect. In your solution it doesn't matter, but
    you'd catch one more potential bug by actually keeping track
    of ingredients, i.e.

        * arbiter doesn't just count ingredients, it collects a
          list of ingredients (you include the Item atom in the message)

        * The {table_full, self()} message includes the list, i.e.
          {table_full, Items, self()}

        * The smoker's receive clause checks that it really has
          all the items, for instance

            receive
                  {table_full, Items, Arbiter} ->
                      [] = [match, paper, tobacco] -- [Item|Items],
                      ...

     Specifically, you would have noticed your tobbacco [sic] typo.

> While we're at it, how would you go about checking that a particular
> solution is actually correct for the problem being solved, i.e. how
> can I systematically check that my code is _right_?

You say "systematically", so you're really providing the answer yourself.

The field of "formal methods" is where you find all the people who are into
systematically checking things. There are various people around who have
done that specifically with Erlang, the two active groups I'm aware of
are

  http://www.chalmers.se/cse/EN/research/research-groups/formal-methods/

and

  http://www.dcs.shef.ac.uk/~qiang/forse/forse.htm

Matt

 * But: my opinion isn't worth much. I'm often rash and careless. I do 
   things like write "Two comments" and then provide three.

   Thomas Arts once used model checking methods to examine a part of
   the control system for some hardware I work on. I was completely
   confident it was bug-free: I wrote it on a day where I turned off
   my mobile phone and shut the door. And it had a good test
   suite. And it'd been running in thousands of switches all over the
   world, in hospitals and in nuclear reactors, for years, and never
   failed. It's A-grade premium battle-tested code with a gold star.

   Thomas and his model checker found a bug, of course, otherwise
   I wouldn't have bothered recounting this. My ego was on life support
   until I managed to show that the bug, like your tobbacco spelling,
   didn't matter. ;-)