SePi issueshttps://git.lasige.di.fc.ul.pt/gloss/SePi/-/issues2018-08-03T14:49:40+01:00https://git.lasige.di.fc.ul.pt/gloss/SePi/-/issues/5Termination in a deadlocked state2018-08-03T14:49:40+01:00Vasco T. VasconcelosTermination in a deadlocked stateCurrently SePi does not distinguish normal termination from termination due to a deadlocked situation.
This process terminates successfully
<pre>
new x y : *!integer
x!77
</pre>
even though in the end there is a process in the x-...Currently SePi does not distinguish normal termination from termination due to a deadlocked situation.
This process terminates successfully
<pre>
new x y : *!integer
x!77
</pre>
even though in the end there is a process in the x-y channel queue. This is ok for x-y is unrestricted. In this case, I suggest that we leave the final message of the interpreter as is:
<pre>
<terminated>
</pre>
This process terminates in a a deadlocked situation:
<pre>
new x y : !integer.end
x!5. y?x
</pre>
In the end, there is a process in the x-y channel queue. But x-y is linear. In this case I suggest that the interpreter ends with something like this:
<pre>
<deadlock on channel x-y>
</pre>
Similarly, at the end of the run of this process
<pre>
new w1 r1 : !integer.end
new w2 r2 : !integer.end
w1!5. w2!7 |
r2?x. r1?y
</pre>
we should read
<pre>
<deadlock on channels w1-x1 and w2-x2>
</pre>Juliana FrancoJuliana Francohttps://git.lasige.di.fc.ul.pt/gloss/SePi/-/issues/4Delegation and the "remaining" channel at end type2018-08-03T14:49:40+01:00Vasco T. VasconcelosDelegation and the "remaining" channel at end typeThis program compiles:
`new x y: !integer.end
if true then x!4 else x!5
|
y?z`
Now if one delegates channel x on one the branches:
`def p z: !integer.end = z!5
new x y: !integer.end
if true then x!4 else p!x
|
y?z`
the...This program compiles:
`new x y: !integer.end
if true then x!4 else x!5
|
y?z`
Now if one delegates channel x on one the branches:
`def p z: !integer.end = z!5
new x y: !integer.end
if true then x!4 else p!x
|
y?z`
then program does not compile anymore. Instead the compiler outputs "The sets of linear channel end must be equal in branches: x".
Now, if we delegate `x` on both branches, then the program compiles again:
`def p z: !integer.end = z!5
new x y: !integer.end
if true then p!x else p!x
|
y?z`
I believe the problem has to do with the fact that on the `then` branch the symbol table has `x:end`, whereas on the `else` branch it has no entry for for variable `x`.
Can we not add an entry `x:colon` to the symbol table when delegating a `x`? There is no reason for the second program not to compile. And if "procedure" `p` is a complex one and cannot be inlined, then the programmer is forced to write a procedure just to keep the compiler happy.Juliana FrancoJuliana Francohttps://git.lasige.di.fc.ul.pt/gloss/SePi/-/issues/2A new cannel called printBoolean causes an internal error2018-08-03T14:49:40+01:00Vasco T. VasconcelosA new cannel called printBoolean causes an internal errorThis seems to be the smallest program that causes the error
`def printBoolean e: end =
printInteger!5
new e _: end
printBoolean!e`
Run the code and you'll get the error below
`java.lang.UnsupportedOperationException: Intern...This seems to be the smallest program that causes the error
`def printBoolean e: end =
printInteger!5
new e _: end
printBoolean!e`
Run the code and you'll get the error below
`java.lang.UnsupportedOperationException: Internal error. This should not happen. The interpreter tried to print a variable. Please contact the development team.
<terminated>`
My intuition is that the problem has to do with the fact that the compiler is accepting a new channel with the name of a primitive channel. I was not expecting the program to compile. In fact I thought type checking would start with the six (I believe) primitive channels on the symbol table, so that the re-declaration of printBoolean would result in a standard error:
`duplicate variable printBoolean`
Juliana FrancoJuliana Francohttps://git.lasige.di.fc.ul.pt/gloss/SePi/-/issues/1Duplicated error message2018-08-03T14:49:40+01:00Vasco T. VasconcelosDuplicated error messageThe following code
new x y : !integer.?boolean.end
x!1 | y?z.y!true
prints twice the same error message
-The type of variable x is still linear at the end of the scope: lin?(boolean).end
-The type of variable x is still linear...The following code
new x y : !integer.?boolean.end
x!1 | y?z.y!true
prints twice the same error message
-The type of variable x is still linear at the end of the scope: lin?(boolean).end
-The type of variable x is still linear at the end of the scope: lin?(boolean).endJuliana FrancoJuliana Franco