Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

mutex(opA) not defined in language manual #27

Closed
mortenhaahr opened this issue Jan 24, 2023 · 25 comments
Closed

mutex(opA) not defined in language manual #27

mortenhaahr opened this issue Jan 24, 2023 · 25 comments

Comments

@mortenhaahr
Copy link

Hi,

When I was studying for my exam I noticed that the language manual does not define the behavior of writing mutex(opA) as a permission predicate, i.e., that opA is to be executed mutually exclusively to itself.

I suggest 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."

Furthermore, I suggest editing the example below the paragraph to include mutex(opA) (and changing the translated permission predicate accordingly).

@nickbattle
Copy link
Contributor

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

@tomooda ?

@tomooda
Copy link
Member

tomooda commented Jan 25, 2023

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

@nickbattle
Copy link
Contributor

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

@nlmave
Copy link
Contributor

nlmave commented Jan 26, 2023 via email

@tomooda
Copy link
Member

tomooda commented Jan 26, 2023

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.

@mortenhaahr
Copy link
Author

@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.

@tomooda
Copy link
Member

tomooda commented Jan 27, 2023

@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)

@nickbattle
Copy link
Contributor

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

@tomooda
Copy link
Member

tomooda commented Jan 27, 2023

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

@nickbattle
Copy link
Contributor

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?

@tomooda
Copy link
Member

tomooda commented Jan 27, 2023

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;

@nickbattle
Copy link
Contributor

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?

@pglvdm
Copy link
Contributor

pglvdm commented Jan 27, 2023

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

per Op => #active(Op) = 0

@nickbattle
Copy link
Contributor

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

@pglvdm
Copy link
Contributor

pglvdm commented Jan 27, 2023

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...

@nickbattle
Copy link
Contributor

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.

@tomooda
Copy link
Member

tomooda commented Jan 27, 2023

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

@nickbattle
Copy link
Contributor

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.

@tomooda
Copy link
Member

tomooda commented Jan 30, 2023

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?

@pglvdm
Copy link
Contributor

pglvdm commented Jan 31, 2023

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!

@tomooda
Copy link
Member

tomooda commented Jan 31, 2023

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.

@mortenhaahr
Copy link
Author

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."

@tomooda
Copy link
Member

tomooda commented Jan 31, 2023

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

tomooda added a commit to tomooda/documentation that referenced this issue Feb 19, 2023
tomooda added a commit that referenced this issue Feb 19, 2023
add explanations of mutex as discussed in #27
@tomooda
Copy link
Member

tomooda commented Feb 19, 2023

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

@mortenhaahr
Copy link
Author

Great! I am closing this issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

5 participants