mutex(opA) not defined in language manual about documentation HOT 25 CLOSED

@mortenhaahr , yes, that addition is also helpful. Thank you for reminding me of it!

from documentation.

Yes, you're right, it doesn't make this clear and it should. Thanks for raising it.

@tomooda ?

from documentation.

I agree to make it clearer, and I have one question:
Given mutex(opA), can opA recurse?

from documentation.

Hmm. Well, who knows what the "rules" are here, but both VDMJ and VDMTools don't allow mutex(op) to recurse:

class A
operations
	public op: nat ==> nat
	op(a) == if a = 0 then return 1 else return a * op(a-1);
	
sync
	mutex(op)

end A

> p new A().op(5)
Exception: DEADLOCK detected

>> p new A().op(5)
No precise position information available:
  Run-Time Error 263: Deadlock is detected

from documentation.

from documentation.

Traditionally, mutex is a pair of atomic counting operations of in/out as @nlmave commented. These days some languages/libraries also provide recursive mutex (e.g. std::recursive_mutex in C++) for synchronization allowing recursion. Considering that the current description in the LRM goes along the syntactic definition mutex predicate = ‘mutex’, ‘(’, (‘all’ | name list, ‘)’ ;, how about changing the passage to the below?

A mutex predicate allows the user to specify either that all operations of the class are to be executed mutually exclusive, or that a list of operations are to be executed mutually exclusive to each other. It is noted that every operation referred to in a mutex is to be executed mutually exclusive also to itself, hence a recursive call of a mutexed operation will result in deadlock once executed.

from documentation.

@tomooda please correct me if I am wrong. But is your suggestion not a bit misleading, as writing mutex(opA, opB) does not enforce opA and opB to be executed mutually exclusive to themselves but only to each other?

As I understand it, the behavior of mutex with a single parameter is entirely different compared to providing a name list or all.

from documentation.

@mortenhaahr Oh, I didn't know the difference in the semantics between a single operation and multiple operations specified.

Indeed it shows complex behavior. With multiple operations specified in a mutex, self-recursion is OK, but mutual recursion between two operations makes deadlock. Hmm.

class A
operations
	public op: nat ==> nat
	op(a) == if a = 0 then return 1 else return a * op(a-1);
	public op1: nat ==> nat
	op1(a) == if a = 0 then return 1 else return a * op2(a-1);
	public op2: nat ==> nat
	op2(a) == if a = 0 then return 1 else return a * op1(a-1);

sync
	mutex(op, op1, op2)

end A

> p new A().op(5)
= 120
Executed in 0.008 secs.
> p new A().op1(5)
DEADLOCK detected
Stopped in 'A' (t.vdmpp) at line 11:5
11: mutex(op, op1, op2)

from documentation.

Hmm... as Marcel said, the mutex is syntactic sugar, and is translated into a permission predicate over the operation(s) concerned. I think this is in line with what the LRM says in section 14.1, though perhaps there is something missing?

In the example above, each operation gets a predicate like per opX => #active(opY) = 0 and #active(opZ) = 0, ie. "the other two aren't running". With a single operation in the mutex, you get per op => #active(op) = 0, which is a different case and explicitly checked for in the translation.

So yes, with multiple operations in the mutex you are allowed to recurse, in VDMJ. But is that as intended? I note that VDMTools has a different interpretation, deadlocking a recursion too. @tomooda, can you find out how this is translated into per-clauses?

>> p new A().op(5)
No precise position information available:
  Run-Time Error 263: Deadlock is detected

from documentation.

Maybe per #active(op, op1, op2) = 0 ?

from documentation.

That makes some sense, but it's not what the example translation in the LRM says/implies. Can/did you check the actual VDMTools translation?

from documentation.

VDMTools/spec/cg-spec/mod_conc.vdm seems to define the translation.
Below is the explanation in the literated spec.

Example of expansion of mutex definition to map of mutex constraints:
\begin{alltt}
  mutex(A,B,C);       { {A,B,C},        { A |-> {A,B,C},
  mutex(A,B);   ->      {A,B},     ->     B |-> {A,B,C},
  mutex(C,D,E);         {C,D,E} }         C |-> {A,B,C,D,E},
                                          D |-> {C,D,E},
                                          E |-> {C,D,E} }
\end{alltt}

I also found a PDF document on vice (in Japanese) telling that

sync
mutex(opA, opB);
mutex(opB, opC, opD);
per opD => someVariable > 42;

will be translated into the below

sync
per opA => #active(opA) + #active(opB) = 0;
per opB => #active(opA) + #active(opB) = 0 and
#active(opB) + #active(opC) + #active(opD) = 0;
per opC => #active(opB) + #active(opC) + #active(opD) = 0;
per opD => #active(opB) + #active(opC) + #active(opD) = 0
and
someVariable > 42;

from documentation.

Interesting. Thanks for looking this up, Tomo. The example from the VDM spec makes sense, but it doesn't explicitly cover the single operation case - though surely it would just say { X |-> {X} }?

The PDF example is more interesting because it is almost the same as the LRM example, except the translations include the "LHS" of each operation, whereas the LRM does not. So it looks like VDMJ is implementing the LRM scheme (probably based on the earlier CSK documentation), whereas VDMTools is implementing the example above.

Ironically, it would be easier to do things the VDMTools way, because there is no special case for a single operation.

I think the only difference is the case of recursion? Do we have any other sources for the correct VDM++ semantics here?

from documentation.

Using #mutex(Op) should definitely not allow Op to recurse since this should be syntactic sugar for:

per Op => #active(Op) = 0

from documentation.

Thanks Peter. What do you think the translations of mutex(op1, op2) should be?

from documentation.

class A
operations
public op1: nat ==> nat
op1(a) == if a = 0 then return 1 else return a * op2(a-1);
public op2: nat ==> nat
op2(a) == if a = 0 then return 1 else return a * op1(a-1);

sync
mutex(op1, op2)

end A

should be a shorthand for:

class A
operations
public op1: nat ==> nat
op1(a) == if a = 0 then return 1 else return a * op2(a-1);
public op2: nat ==> nat
op2(a) == if a = 0 then return 1 else return a * op1(a-1);

sync
per op1 => #active(op2) = 0
per op2 => #active(op1) = 0

end A
Essentially that all other operations cannot be active...

from documentation.

OK, that's what the LRM says and VDMJ implements, but VDMTools (including its documents and spec) is slightly different, including the LHS operation in each #active - so per op1 => #active(op1, op2) = 0 and the same for op2. This means VDMJ will allow recursion with a mutex over two ops, whereas VDMTools will not.

from documentation.

Please correct if I say wrong. Does the current VDMJ allow multiple threads to execute A`op1() concurrently even with sync mutex(op1, op2)?

from documentation.

The #active count is across all threads for one object instance. So per op1 => #active(op2) = 0ought to allow any number of concurrent op1 calls on a given instance, as long as there are no op2s active; but the mutex also creates per op2 => #active(op1) = 0, so you could also call any number of concurrent op2s, unless there was an op1.

Hmm. So it's a sort of concurrent mutex, as things stand. I haven't actually tried this!

Presumably the VDMTools interpretation only allows one thread to be calling op1 or op2? That is closer to what I thought a mutex should be doing, I must admit. The wording in the LRM is not clear at all, unfortunately.

from documentation.

I think we understand the problem, but I don't see a single obvious solution. The definition in the LRM is incomplete because it does not cover a mutex on a single operation and also has a tricky difference from mutex used in other languages. VDMJ's implementation agrees with the LRM's mutex expansion rule and shares the same difference from the common mutex. VDMTools' implementation agrees with other languages' mutex but breaks compatibility with VDM10's semantics.
I think the LRM needs revision. However, it's not clear what it should be. Maybe an RC?

from documentation.

Well in the VDM++ book from 2005 in the chapter on concurrency it is VERY clear what mutex(Op1) means on page 285. IMHO there should be NO need to have a RC for something that has been clear since then!

from documentation.

Okay, I confirmed that mutex(Put, Get) is equivalent to per Put => #active(Get) = 0; per Get => #active(Put) = 0 in Excercise 12.1 and its answer in the book (Japanese translation). I agree that no RC is needed.

So, as @mortenhaahr proposed at the very beginning, adding a complementary explanation and an example would be enough. How about the below?

sync
 mutex(opA, opB);
 mutex(opB, opC, opD);
 mutex(opD);
 per opD => someVariable > 42;

would be translated to the following permission predicates:

sync
 per opA => #active(opB) = 0;
 per opB => #active(opA) = 0 and
            #active(opC) + #active(opD) = 0;
 per opC => #active(opB) + #active(opD) = 0;
 per opD => #active(opB) + #active(opC) = 0 and
            #active(opD) = 0 and
            someVariable > 42;

As shown in the translated per clauses, a mutex on multiple operations is translated to a set of permission predicates each of which blocks the execution of an operation when any one of the other operations is being executed. Please note that a mutex on multiple operations does not prevent multiple executions of any one of the operations. A mutex on a single operation, such as mutex(opD) in the above example, blocks multiple executions of the operation.

@mortenhaahr , thank you for raising this issue. I might have messed up quite a bit, but this was really a good learning opportunity for me :-)
I used opD instead of opA in the example because I'm a little afraid that per opA => #active(opB) = 0 and #active(opA) = 0; might be confusing.

from documentation.

I think the suggested addition looks great. And no worries @tomooda, it led to a very interesting discussion.

In addition to what you proposed, I also suggest changing the introductory line as indicated in the beginning.

I.e., changing the line:
"A mutex predicate allows the user to specify either that all operations of the class are to be executed mutually exclusive, or that a list of operations are to be executed mutually exclusive to each other."

to:
"A mutex predicate allows the user to specify either that all operations of the class are to be executed mutually exclusive, an operation is to be executed mutually exclusive to itself, or that a list of operations is to be executed mutually exclusive to each other."

from documentation.

Okay, I made a PR #28 and merged it into the editing branch.

from documentation.

Great! I am closing this issue.

from documentation.