Semantics for multi-thread program - #73
Conversation
|
|
||
| Variable (es : cexec_event_struct). | ||
| Notation dom := (dom es). | ||
| Notation domain := (dom es). |
There was a problem hiding this comment.
Why do you change the name here? It's very confusing.
| @@ -215,12 +216,20 @@ Definition add_hole | |||
|
|
|||
| Definition eval_step (c : config) {pr : E} | |||
There was a problem hiding this comment.
Why pr is implicit?
Here and above too.
| [:: Config (evstr c) [fsfun c with pr |-> cont_st inh]]. | ||
| Variable prog : parprog. | ||
|
|
||
| Definition fresh_tid (c : config) : nat := |
There was a problem hiding this comment.
Here we can't just take codom of tmap because to do this it's codom should be choiceType
There was a problem hiding this comment.
I guess you're talking about codomf
https://github.com/math-comp/finmap/blob/1fc012fc8f0dfe494708a2775931bc40682c2c9e/finmap.v#L3473
Yes, this one required the type of codomain V : choiceType. It then obtains the codomain as fset.
Thus we cannot use codomf here.
However, we don't need to get the codomain in the form of fset here.
The fsfun is based on finmap which in turn is just a finfun.
https://github.com/math-comp/finmap/blob/1fc012fc8f0dfe494708a2775931bc40682c2c9e/finmap.v#L2887
finfun can be converted to a tuple.
I guess here is the function you need, but perhaps there is an easier way (@anton-trunov we need your advice here).
https://github.com/math-comp/math-comp/blob/63007afd537608e64dad3f754bb8d6986a042b17/mathcomp/ssreflect/finfun.v#L277
From a tuple you can easily get the codomain as a list (seq), then use map to project to a second component (tid) and from there you can get the thread id's as a finite set if you'll need.
There was a problem hiding this comment.
I think fgraph is the most suitable for our goal. You can watch how does it look now
| (e, v) <- add_hole l pr; | ||
| [:: Config e [fsfun c with fresh_id |-> (cont_st v, tid)]] | ||
| else | ||
| [:: Config es [fsfun c with pr |-> (cont_st inh, tid)]]. |
There was a problem hiding this comment.
Look much better now, good job.
| end. | ||
|
|
||
| Definition ltr_thrd_sem (l : option (@label V V)) pgm st1 st2 : bool := | ||
| match thrd_sem pgm st1, l with |
There was a problem hiding this comment.
Shouldn't you now also handle ThreadStart case?
2 participants
In this PR our semantics of one-thread program was upgraded to the semantics of multi-thread program.
Here were made some technical things, and it is a bit difficult for me to explain the main problem offline. I think the better way would be to discuss this PR at the meeting
I don't know if my solution is a good idea, but anyway it is temporal: we are going to get rid of programs with fixed number of threads from the very beginning