Deadlocking using very simple Get & Put operations #17
Description
Problem
The tuple spaces seems to be deadlocking by using very simple Get/Put requests (see the attached go program). The following test script has been checked for deadlocks in Spin and it shouldn't deadlock.
Possible solution?
By looking into the library, it seems to something with locking/unlocking the WaitingClients. By changning when it's locked and unlocked on both Get and Put seems be a simple fix, but it makes the application slower.
Scripts
// testfile.go
package main
import (
"fmt"
"github.com/pspaces/gospace/space"
)
func main() {
spc1 := space.NewSpace("space")
spc1.Put("ready")
go func() {
i := 0
for {
spc1.Get("state")
fmt.Println("P2 Got state", i)
i++
spc1.Put("ready")
}
}()
go func() {
i := 0
for {
_, err := spc1.GetP("ready")
if err == nil {
spc1.Put("state")
fmt.Println("P1 Put state", i)
i++
} else {
fmt.Errorf("Unable to receive ready")
}
}
}()
<-make(chan bool)
}// Spin model check
#define N 1
mtype = {state,ready}
chan spc = [N] of { mtype }
active proctype p1(){
do ::spc!ready
do::
spc?state
printf("got state\n")
spc!ready
printf("put ready\n")
od
od
}
active proctype p2(){
do ::spc?ready
printf("got ready\n")
spc!state
printf("put state\n")
::else ->
od
}