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

[ base ] Add non-blocking and timeout variants for channelGet #3435

Open
wants to merge 55 commits into
base: main
Choose a base branch
from
Open
Changes from 54 commits
Commits
Show all changes
55 commits
Select commit Hold shift + click to select a range
a4aae0a
Initial implementation of non-blocking version of blodwen-channel-get.
Matthew-Mosior Nov 25, 2024
f261821
Adding channelGetNonBlocking function to System.Concurrency.idr (non-…
Matthew-Mosior Nov 25, 2024
68ecf8b
Adding matching mutex-release call to initial mutex-acquire call.
Matthew-Mosior Nov 25, 2024
89f7991
Fixing indentation in blodwen-channel-get-non-blocking.
Matthew-Mosior Nov 25, 2024
9381947
Adding matching mutex-release call to initial mutex-acquire call (aga…
Matthew-Mosior Nov 25, 2024
a5610fa
Fixing return values for blodwen-channel-get-non-blocking.
Matthew-Mosior Nov 25, 2024
fb04471
Fixing extern type signature and channelGetNonBlocking function, alon…
Matthew-Mosior Nov 25, 2024
9a53f9a
Removing blocking aspect from blodwen-channel-get-non-blocking.
Matthew-Mosior Nov 25, 2024
818c5ba
Fixing styling of blodwen-channel-get-non-blocking.
Matthew-Mosior Nov 25, 2024
fe1dd2d
Removing extra mutex-release call.
Matthew-Mosior Nov 25, 2024
8754137
Removing duplicate val calls.
Matthew-Mosior Nov 25, 2024
7936ae1
Fixing return type.
Matthew-Mosior Nov 25, 2024
45dfec5
Fixing return type.
Matthew-Mosior Nov 25, 2024
21e877a
Fixing channelGetNonBlocking.
Matthew-Mosior Nov 25, 2024
82defee
Reverting return type fix.
Matthew-Mosior Nov 25, 2024
af8f499
Removing unnecessary comments.
Matthew-Mosior Nov 25, 2024
dbf8e83
Remove incorrect documentation.
Matthew-Mosior Nov 25, 2024
fadb1e9
Altering blodwen-channel-get-non-blocking to error when mutex cant be…
Matthew-Mosior Nov 25, 2024
fb8fb26
Cleaning up commented out code.
Matthew-Mosior Nov 25, 2024
2b6077b
Adding blodwen-channel-check scheme function to enable correct handli…
Matthew-Mosior Nov 25, 2024
f8c24af
Optimizing blodwen-channel-get-non-blocking.
Matthew-Mosior Nov 26, 2024
9e7ba48
Changing Boolean comparision to Int (compatible with expected Prim ty…
Matthew-Mosior Nov 26, 2024
0684a10
Adding decoding support for channelGetNonBlocking.
Matthew-Mosior Nov 27, 2024
56d42bd
Removing extra %foreign pragmas.
Matthew-Mosior Nov 27, 2024
e8a39f3
Removing extra %foreign.
Matthew-Mosior Nov 27, 2024
5a18386
Fixing blodwen-channel-get-non-blocking by removing extra set of pare…
Matthew-Mosior Nov 27, 2024
6e8c4a5
Adding channelGetNonBlocking test.
Matthew-Mosior Nov 27, 2024
0c4b2dd
Changing 0 to () for the return on failed mutex acquisition or an emp…
Matthew-Mosior Nov 27, 2024
042799d
Removing extraneous whitespace.
Matthew-Mosior Nov 27, 2024
636ca50
Removing unnecessary scheme decoding.
Matthew-Mosior Nov 27, 2024
2d1b96c
Fixing initial channelGetNonBlocking test.
Matthew-Mosior Nov 27, 2024
4a4699f
Fixing indentation for blodwen-channel-get-non-blocking.
Matthew-Mosior Nov 27, 2024
5db18d8
Adding back decoding support, fixing blodwen-channel-get-non-blocking…
Nov 28, 2024
87265de
Adding another test for channelGetNonBlocking.
Nov 28, 2024
714e5b1
Removing tabs from blodwen-channel-get-non-blocking.
Nov 28, 2024
126a52a
Adding initial skeleton for blodwen-channel-get-with-timeout.
Dec 2, 2024
8d78679
Adding initial blodwen-channel-get-with-timeout function and associat…
Matthew-Mosior Dec 3, 2024
b3fa699
Fixing small issue with blodwen-channel-get-with-timeout.
Dec 3, 2024
8ee6e4b
Adding corrected blodwen-channel-get-with-timeout implementation and …
Dec 4, 2024
fdc11b6
Updating documentation for channelGetWithTimeout function.
Dec 4, 2024
98b485a
Adding Scheme Nat implementation and fixing test.
Dec 4, 2024
8eb7457
Re-ordering imports for channel007 test.
Dec 4, 2024
4f85729
Adding changes of this PR to CHANGELOG_NEXT.md.
Dec 4, 2024
80fafa9
Merge branch 'main' into Issue-3424
Matthew-Mosior Dec 4, 2024
474bd6b
Fixing linting issues.
Dec 4, 2024
cd24d35
Adding additional sleep in channel007 test.
Dec 4, 2024
970ace4
Addressing comments.
Dec 5, 2024
0a79b46
Addressing comments (fixed).
Dec 5, 2024
6a5129f
Addressing comments (tests).
Dec 5, 2024
917b240
Fixing linting.
Dec 5, 2024
2a70bad
Addressing comments.
Matthew-Mosior Dec 6, 2024
6b13dc8
Addressing @cypheon's comments.
Matthew-Mosior Dec 7, 2024
fa50df7
Removing duplicate tests from allscheme.
Matthew-Mosior Dec 7, 2024
ef41d27
Merge branch 'main' into Issue-3424
Matthew-Mosior Dec 13, 2024
eddaf30
Changing Nat to Int for FFI type on prim__channelGetWithTimeout.
Matthew-Mosior Jan 7, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion CHANGELOG_NEXT.md
Original file line number Diff line number Diff line change
@@ -265,6 +265,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
* Refactored `Uninhabited` implementation for `Data.List.Elem`, `Data.List1.Elem`, `Data.SnocList.Elem` and `Data.Vect.Elem`
so it can be used for homogeneous (===) and heterogeneous (~=~) equality.

* Added `System.Concurrency.channelGetNonBlocking` for the chez backend.

* Added `System.Concurrency.channelGetWithTimeout` for the chez backend.

#### Contrib

* `Data.List.Lazy` was moved from `contrib` to `base`.
@@ -306,7 +310,6 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO

* Add a missing function parameter (the flag) in the C implementation of `idrnet_recv_bytes`


#### Test

* Replaced `Requirement` data type with a new record that can be used to create
25 changes: 21 additions & 4 deletions libs/base/System/Concurrency.idr
Original file line number Diff line number Diff line change
@@ -72,19 +72,15 @@ data Condition : Type where [external]
%foreign "scheme,racket:blodwen-make-cv"
"scheme,chez:blodwen-make-condition"
prim__makeCondition : PrimIO Condition

%foreign "scheme,racket:blodwen-cv-wait"
"scheme,chez:blodwen-condition-wait"
prim__conditionWait : Condition -> Mutex -> PrimIO ()

%foreign "scheme,chez:blodwen-condition-wait-timeout"
-- "scheme,racket:blodwen-cv-wait-timeout"
prim__conditionWaitTimeout : Condition -> Mutex -> Int -> PrimIO ()

%foreign "scheme,racket:blodwen-cv-signal"
"scheme,chez:blodwen-condition-signal"
prim__conditionSignal : Condition -> PrimIO ()

%foreign "scheme,racket:blodwen-cv-broadcast"
"scheme,chez:blodwen-condition-broadcast"
prim__conditionBroadcast : Condition -> PrimIO ()
@@ -187,6 +183,10 @@ data Channel : Type -> Type where [external]
prim__makeChannel : PrimIO (Channel a)
%foreign "scheme:blodwen-channel-get"
prim__channelGet : Channel a -> PrimIO a
%foreign "scheme,chez:blodwen-channel-get-non-blocking"
prim__channelGetNonBlocking : Channel a -> PrimIO (Maybe a)
%foreign "scheme,chez:blodwen-channel-get-with-timeout"
prim__channelGetWithTimeout : Channel a -> Nat -> PrimIO (Maybe a)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Last I checked Nat was not a blessed primitive type for passing via the FFI (https://idris2.readthedocs.io/en/latest/ffi/ffi.html#primitive-ffi-types). What that means in practice is that if it works then it "just happens to work" even though Nat may in practice be implemented in a way that is compatible with Int for any given backend.

Someone could correct me here, but best practice would be to use Nat in your exported code but cast to Int for your FFI call.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@mattpolzin

Awesome catch here, I've addressed this via eddaf30

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@mattpolzin

It looks like all tests passed but one:

https://github.com/idris-lang/Idris2/actions/runs/12659854176/job/35280037440?pr=3435

It looks like it timed out, but not sure if that is supposed to happen?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It shouldn't time out but that's not unheard of so I've just kicked tests off again.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for kicking off the tests again, looks like it all passed this time.

%foreign "scheme:blodwen-channel-put"
prim__channelPut : Channel a -> a -> PrimIO ()

@@ -208,6 +208,23 @@ export
channelGet : HasIO io => (chan : Channel a) -> io a
channelGet chan = primIO (prim__channelGet chan)

||| Non-blocking version of channelGet (chez backend).
|||
||| @ chan the channel to receive on
partial
export
channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a)
channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan)

||| Timeout version of channelGet (chez backend).
|||
||| @ chan the channel to receive on
||| @ milliseconds how many milliseconds to wait until timeout
partial
export
channelGetWithTimeout : HasIO io => (chan : Channel a) -> (milliseconds : Nat) -> io (Maybe a)
channelGetWithTimeout chan milliseconds = primIO (prim__channelGetWithTimeout chan milliseconds)

||| Puts a value on the given channel.
|||
||| @ chan the `Channel` to send the value over
55 changes: 54 additions & 1 deletion support/chez/support.ss
Original file line number Diff line number Diff line change
@@ -439,6 +439,60 @@
(condition-signal read-cv)
the-val))

(define (blodwen-channel-get-non-blocking ty chan)
(if (mutex-acquire (channel-read-mut chan) #f)
(let* ([val-box (channel-val-box chan)]
[read-box (channel-read-box chan)]
[read-cv (channel-read-cv chan)]
[the-val (unbox val-box)]
)
(if (null? the-val)
(begin
(mutex-release (channel-read-mut chan))
'())
(begin
(set-box! val-box '())
(set-box! read-box #t)
(mutex-release (channel-read-mut chan))
(condition-signal read-cv)
(box the-val))
))
'()))

(define (blodwen-channel-get-with-timeout ty chan timeout)
(let loop ()
(let* ([sec (div timeout 1000)])
(if (mutex-acquire (channel-read-mut chan) #f)
(let* ([val-box (channel-val-box chan)]
[val-cv (channel-val-cv chan)]
[the-val (unbox val-box)])
(if (null? the-val)
(begin
;; Wait for the condition timeout
(condition-wait val-cv (channel-read-mut chan) (make-time 'time-duration 0 sec))
(let* ([the-val (unbox val-box)]) ; Check again after wait
(if (null? the-val)
(begin
(mutex-release (channel-read-mut chan))
'()) ; Still empty after timeout
(let* ([read-box (channel-read-box chan)]
[read-cv (channel-read-cv chan)])
;; Value now available
(set-box! val-box '())
(set-box! read-box #t)
(mutex-release (channel-read-mut chan))
(condition-signal read-cv)
(box the-val)))))
(let* ([read-box (channel-read-box chan)]
[read-cv (channel-read-cv chan)])
;; Value available immediately
(set-box! val-box '())
(set-box! read-box #t)
(mutex-release (channel-read-mut chan))
(condition-signal read-cv)
(box the-val))))
loop)))) ; Failed to acquire mutex

Matthew-Mosior marked this conversation as resolved.
Show resolved Hide resolved
;; Mutex

(define (blodwen-make-mutex)
@@ -499,7 +553,6 @@
(define (blodwen-clock-second time) (time-second time))
(define (blodwen-clock-nanosecond time) (time-nanosecond time))


(define (blodwen-arg-count)
(length (command-line)))

24 changes: 24 additions & 0 deletions tests/chez/channels007/Main.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
import System
import System.Concurrency

-- Test that using channelGetNonBlocking works as expected.
main : IO ()
main = do
chan <- makeChannel
threadID <- fork $ do
channelPut chan "Hello"
channelPut chan "Goodbye"
sleep 1
case !(channelGetNonBlocking chan) of
Nothing => putStrLn "Nothing"
Just val' => putStrLn val'
sleep 1
case !(channelGetNonBlocking chan) of
Nothing => putStrLn "Nothing"
Just val' => putStrLn val'
sleep 1
case !(channelGetNonBlocking chan) of
Nothing => putStrLn "Nothing"
Just val' => putStrLn val'
sleep 1

3 changes: 3 additions & 0 deletions tests/chez/channels007/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Hello
Goodbye
Nothing
3 changes: 3 additions & 0 deletions tests/chez/channels007/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
. ../../testutils.sh

run Main.idr
23 changes: 23 additions & 0 deletions tests/chez/channels008/Main.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
import Data.Maybe
import System
import System.Concurrency

-- Simple producing thread.
producer : Channel Nat -> Nat -> IO ()
producer c n = ignore $ producer' n
where
producer' : Nat -> IO ()
producer' Z = pure ()
producer' (S n) = do
channelPut c n
sleep 1

-- Test that channelGetWithTimeout works as expected.
main : IO ()
main =
do c <- makeChannel
tids <- for [0..11] $ \n => fork $ producer c n
vals <- for [0..11] $ \_ => channelGetWithTimeout c 5000
ignore $ traverse (\t => threadWait t) tids
putStrLn $ show $ sum $ fromMaybe 0 <$> vals

1 change: 1 addition & 0 deletions tests/chez/channels008/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
55
3 changes: 3 additions & 0 deletions tests/chez/channels008/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
. ../../testutils.sh

run Main.idr
Loading