feat: socket support using LibUV #6683

algebraic-dev · 2025-01-17T23:53:06Z

This PR introduces TCP socket support using the LibUV library, enabling asynchronous I/O operations with it.

Co-authored-by: Henrik Böving <[email protected]>

This PR adds support for `Timer` and a event loop thread that gets requests from another threads and executes it. --------- Co-authored-by: Markus Himmel <[email protected]> Co-authored-by: Henrik Böving <[email protected]>

This PR implements a basic asynchronous timer API on top of the libuv work. It purposely puts this into `Std.Internal` as we might still have to change the API as we continue develop of the async library across releases so I would only like to stabilize it once we are certain this is a fine API. A few additional notes: - we currently do not implement a bind operator on `AsyncTask` on purpose as `Task.bind` on `Task.pure` is a non trivial operation and users should be aware of it. Furthermore there is the consideration that as they will have to bind on both `IO` and `AsyncTask` we might want to make potential task points explicit in the syntax (did somebody say `await`?). - the API generally takes inspiration from https://docs.rs/tokio/latest/tokio/time/index.html, though it has to adapt as Rust's and Lean's asynchronity concepts are sufficiently different. Stacked on top of leanprover#6219.

m# git update-ref -d MERGE_HEAD

src/runtime/uv/tcp.cpp

leanprover-community-bot · 2025-01-23T05:57:39Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9b629cc81f01642200eb0762da39b2935652754c --onto 9b74c07767dc50645efa00356a7724e7f7176227. (2025-01-23 05:57:38)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 104b3519d79f5996dd6d325cba18d94a4615e418 --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-30 00:33:23)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 104b3519d79f5996dd6d325cba18d94a4615e418 --onto a35bf7ee4c4d900475d88886825a5337f389bd0f. (2025-01-30 00:52:24)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 104b3519d79f5996dd6d325cba18d94a4615e418 --onto e922edfc218090ab2e54092336c67fe3b970dfc2. (2025-01-30 17:26:52)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 104b3519d79f5996dd6d325cba18d94a4615e418 --onto 832d7c500d709deb5e7f0a5a6fd0f01865d1a303. (2025-02-04 04:01:35)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5eca093a89bc7dcd09e54b0a9c71bb3472d66709 --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-08 00:17:56)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2fed93462d964252519aa0d2fcd797f86bb52f7c --onto 2960b384af1f29f566f59a3ede8ac982e4628f19. (2025-02-22 00:32:04)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2fed93462d964252519aa0d2fcd797f86bb52f7c --onto 5cbeb22564c6caa0603612edfdabda4bdb34b780. (2025-02-25 16:51:49)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2fed93462d964252519aa0d2fcd797f86bb52f7c --onto c3402b85ab96b7ceec32e0b119837913da0051d0. (2025-02-26 12:14:54)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2fed93462d964252519aa0d2fcd797f86bb52f7c --onto 727c696d9f132bc2701b9755f8819bd36335cd26. (2025-02-27 23:20:20)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2fed93462d964252519aa0d2fcd797f86bb52f7c --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-07 22:02:33)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a0acbd77ea784d43d8daab052567da0087b3783c --onto d32a7b250ad20477d55034488d89a050fbf70af5. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-18 01:23:29)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 53fcae031e5a37c7d8c0ac880f4da28929e3b932 --onto d32a7b250ad20477d55034488d89a050fbf70af5. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-18 15:55:39)

hargoniX

I think this is very promising now! There's mostly on memory leaks and stylistic things left but the implementation looks like it should be able to work now.

Beyond these issues it would of course be great if we could also have some tests like for Timer that exercise this API. I would assume you can just connect to localhost and do an echo or something like that? Of course we should have tests for both IPv4 and v6.

After we have those tests I guess it might also be a good idea to write a little benchmark to see how many TCP connections we can handle per second to get an estimate of what kind of load we can expect to handle at best given this implementation.

src/Std/Internal/UV/Tcp.lean

src/runtime/uv/tcp.cpp

…socket

hargoniX

I think the code looks pretty reasonable now, two more things that are generally relevant that I didn't point out:

As previously pointed out it would be nice to have some debug_asserts for all of the implicit invariants that are flying around here.
As previously pointed out we should make it stylistically consistent, currently the pointer * sometimes goes like type * var and other times like type* var (with the third but unused option of course being type *var). We should stick to one style consistently here, I personally prefer type* but we should make that call based on existing code.
I'd like to get a second opinion before we merge the code. I think the implementation is sound logic wise but it could still be possible that we oversaw a failure condition or a memleak.

src/Std/Internal/Async/TCP.lean

src/runtime/uv/tcp.cpp

src/Std/Internal/Async/TCP.lean

src/runtime/uv/net_addr.cpp

src/runtime/uv/tcp.h

src/runtime/uv/tcp.cpp

Co-authored-by: Henrik Böving <[email protected]>

…-socket

hargoniX

Apart from those few nits it's fine to merge now I think.

src/runtime/uv/tcp.cpp

src/runtime/uv/tcp.h

Co-authored-by: Henrik Böving <[email protected]>

…socket

…-socket

algebraic-dev and others added 11 commits January 10, 2025 16:44

feat: implement the basic libuv event loop

b875f26

Co-authored-by: Henrik Böving <[email protected]>

doc: the event loop

7528056

fix: make the cond var safe and document it

50cc599

feat: start of the uv tc

c18310d

feat: basic tcp structure

5726fcd

Merge branch 'ft-async' of github.com:leanprover/lean4 into tcp-socket

f376f93

feat: progress on connection

da8919a

feat: three functions

04621bb

merge branch 'master' of github.com:leanprover/lean4 into tcp-socket

7a1c978

m# git update-ref -d MERGE_HEAD

algebraic-dev requested a review from TwoFX as a code owner January 17, 2025 23:53

algebraic-dev marked this pull request as draft January 17, 2025 23:53

algebraic-dev added 2 commits January 17, 2025 21:02

chore: remove useless comment

260d5cb

chore: remove useless modifications

8e2fe1c

hargoniX requested changes Jan 20, 2025

View reviewed changes

algebraic-dev added 2 commits January 23, 2025 02:33

feat: impl all functions

9c2e66b

fix: namespace brace

c08d70b

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jan 23, 2025

fix: memory leak in accept

889f9cb

hargoniX requested changes Jan 23, 2025

View reviewed changes

algebraic-dev added 8 commits January 23, 2025 15:26

chore: stylistic changes

cc2baa4

chore: small changes

28fe474

chore: remove useless print

6e6016e

chore: comments and messages

abf70f8

chore: move things around

128aec9

Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…

4ec0f5f

…socket

fix: behavior of loop configure function

fdd5599

Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…

9e39fbd

…socket

hargoniX requested changes Mar 7, 2025

View reviewed changes

algebraic-dev added 2 commits March 7, 2025 18:27

fix: small fixes

9ea39c8

chore: fix all pointers code style

59c4505

TwoFX added the release-ci Enable all CI checks for a PR, like is done for releases label Mar 11, 2025

TwoFX reviewed Mar 11, 2025

View reviewed changes

algebraic-dev added 2 commits March 11, 2025 10:53

fix: unlocks in the right place, and comments

a58ca30

chore: fix comment

916cfd7

hargoniX reviewed Mar 11, 2025

View reviewed changes

src/runtime/uv/tcp.cpp Outdated Show resolved Hide resolved

algebraic-dev and others added 10 commits March 11, 2025 13:05

chore: fix signature

ed7c547

Co-authored-by: Henrik Böving <[email protected]>

fix: int32

897e8a1

merge: branch 'tcp-socket' of github.com:algebraic-dev/lean4 into tcp…

426c040

…-socket

fix: problems with windows

7ebccf8

fix: borrows

9576e70

fix: borrow

a842ecd

fix: size of sockaddr_storage

a8aea97

Merge branch 'master' of https://github.com/leanprover/lean4 into tcp…

f2d627c

…-socket

fix: borrows

10c8b04

revert: small change in connect function

bd2ca66

hargoniX requested changes Mar 18, 2025

View reviewed changes

src/runtime/uv/tcp.cpp Outdated Show resolved Hide resolved

src/runtime/uv/tcp.cpp Outdated Show resolved Hide resolved

src/runtime/uv/tcp.cpp Outdated Show resolved Hide resolved

src/runtime/uv/tcp.h Show resolved Hide resolved

algebraic-dev and others added 5 commits March 18, 2025 11:01

chore: grammar

47d4f8d

Co-authored-by: Henrik Böving <[email protected]>

fix: buffer and io worlds

1241b36

Merge branch 'tcp-socket' of github.com:algebraic-dev/lean4 into tcp-…

1c3c00e

…socket

chore: comment

b9feaf9

Merge branch 'master' of https://github.com/leanprover/lean4 into tcp…

826f42f

…-socket

hargoniX approved these changes Mar 18, 2025

View reviewed changes

hargoniX removed the awaiting-review Waiting for someone to review the PR label Mar 18, 2025

fix: lean wasm build

5a15b0c

algebraic-dev added this pull request to the merge queue Mar 19, 2025

Merged via the queue into leanprover:master with commit d7d1754 Mar 19, 2025
21 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: socket support using LibUV #6683

feat: socket support using LibUV #6683

algebraic-dev commented Jan 17, 2025 •

edited by hargoniX

Loading

leanprover-community-bot commented Jan 23, 2025 •

edited

Loading

hargoniX left a comment

hargoniX left a comment •

edited

Loading

hargoniX left a comment

feat: socket support using LibUV #6683

feat: socket support using LibUV #6683

Conversation

algebraic-dev commented Jan 17, 2025 • edited by hargoniX Loading

leanprover-community-bot commented Jan 23, 2025 • edited Loading

hargoniX left a comment

Choose a reason for hiding this comment

hargoniX left a comment • edited Loading

Choose a reason for hiding this comment

hargoniX left a comment

Choose a reason for hiding this comment

algebraic-dev commented Jan 17, 2025 •

edited by hargoniX

Loading

leanprover-community-bot commented Jan 23, 2025 •

edited

Loading

hargoniX left a comment •

edited

Loading