HackerTrans
TopNewTrendsCommentsPastAskShowJobs

wucke13

no profile record

Submissions

EasyTier – P2P mesh VPN written in Rust using Tokio

easytier.cn
158 points·by wucke13·작년·51 comments

comments

wucke13
·지난달·discuss
> I pay 0% capital gain tax and use a broker with nearly 0 fees which allows me to rotate for free (almost)

How so?
wucke13
·2개월 전·discuss
Software distribution for Linux can be hard. Many distros, different conventions, no FHS is long forgotten, ...

However, Xilinx Vivado and Vitis are so obtusely distributed, making it incredibly hard to package them well.

Three random issues I remember:

1. We had a lot of trouble with Vivado projects randomly breaking. The culprit: German localization combined with automatic clock frequency derivation. Depending on which logic blocks where wired up how, you would get i.e. 99.999 MHz instead of 100 MHz. Apparently, Vivado uses a localized printf (or equivalent) to generate TCL scripts. In German localization, the decimal is a comma, which is interpreted as additional argument in the TCL scripts. 2. For simulation, scripts scripts are copied from a template folder to the user folder, and subsequently adjusted. They are copied in archive mode. If the template is read-only to the current user, so is the new copy, thus failing the subsequent adjustment. 3. If you run the installer with --help as argument, it pops up an X window displaying the help. In general, IIRC, we need to run a headless X just to run the installer in CLI/batch mode.

From a Linux distro maintainer perspective, the packaging is horrible. In particular separation of base installation, configuration, and add-ons is non-existent. Large amount of vendored dependencies, only then to depend on the most minute little packages that Ubuntu supposedly ships.

Setting up a reliable, reproducible CI/CD environment based on Vivado is a large headache.

That all goes to say: if anything, AMD/Xilinx should be paying its customers to deal with this. Unless there is a major improvement in the software distribution practices for Linux, I could not justify to my employer paying money for this experience.

On the other hand, if they commercialize on Linux support, there is soooo much that they can improve by a lot, who knows. Hope dies last and all.
wucke13
·9개월 전·discuss
My take: containers forced devepopers to declare various aspects of the application in a standardized, opinioated way:

- Persistant state? Must declare a volume. - IO with external services? Must declare the ports (and maybe addresses). - Configurable parameters? Must declare some env variables. - Trasitive dependecies? Must declare them, but using a mechanism of your choosing (e.g. via the package manager of your base image distro).

Separation of state (as in persistency) and application (as in binaries, assets) makes updates easy. Backups also.

Having most all IO visible and explicit simplifies operation and integration.

And a single, (too?!?) simple config mechanism increases reusability, by enabling e.g. lightweight tailoring of generic application service containers (such as mariadb).

Together this bunch of forced, yet leaky abstractions is just good enough to foster immense reuse & composability on to a plethora of applications, all while allowing to treat them almost entirely like blackboxes. IMHO that is why OCI containers became this big, compared to other virtualization and (application-) cuntainer technologies.
wucke13
·9개월 전·discuss
For the seL4 proofs a subset of C was formalized, for example.

(Already mentioned) CakeML would be another example, together maybe with its Pancake sibling.

Also: WebAssembly!
wucke13
·9개월 전·discuss
That's pohibitively expensive in the general case when external input is used and/or when arithmetic is used on the values (main differerence to sum-types).
wucke13
·9개월 전·discuss
I know quite some people in the safety/aviation domain that kind of dislike the subranges, as it inserts run-time checks that are not easily traceable to source code, thus escaping the trifecta of requirements/tests/source-code (which all must be traceable/covered by each other).

Weirdly, when going through the higher assurance levels in aviation, defensive programming becomes more costly, because it complicates the satisfaction of assurance objectives. SQLite (whiches test suite reaches MC/DC coverage which is the most rigorous coverage criterion asked in aviation) has a nice paragraph on the friction between MC/DC and defensive programming:

https://www.sqlite.org/testing.html#tension_between_fuzz_tes...
wucke13
·9개월 전·discuss
Neither the Rust nor the Ada spec is formal, in the sense of consumable by a theorem prover. AFAIK for Ada Spark, there is of course assumptions on the language semantics built-in to Spark, but: these are nowhere coherently written down in a truly formal (as in machine-readable) spec.
wucke13
·10개월 전·discuss
I think what parent was about is open vs. closed loop control, not fly-by-wire or not. Both their and your point stand of course.
wucke13
·10개월 전·discuss
I have dedicated a large chunk of my (arguably short) professional career on improving upon this, mostly in the safety critical software domain. What was your experience back then, what made you leave ultimately, and what do you do now?
wucke13
·10개월 전·discuss
Rust in particular with miri is quite impressive at catching them. You just run your testcases via

    cargo miri run
And if your code actually touches UB, mirei will most likely point out exactly where and why.
wucke13
·10개월 전·discuss
It doesn't necessarily, but it can. Genode/SculptOS is kind of a microkernel OS framework, and it can use seL4 as the kernel.

Here is a talk about that porting effort:

https://m.youtube.com/watch?v=N624i4X1UDw
wucke13
·10개월 전·discuss
Gernot Heiser would strongly disagree with you on the last one :D
wucke13
·11개월 전·discuss
I'm not so sure, I thought "patch" originated from hole punching cards to program stuff. A software patch was literally a patch of tape that hides an errorneously punched hole in such a card.

The term patch-cable seems to be way younger.
wucke13
·12개월 전·discuss
https://www.pe0sat.vgnet.nl/sdr/iq-data-explained/

This is an excellent introduction to the concept and also to the why complex numbers are used to represent signal samples.
wucke13
·작년·discuss
Is this in effect introducing algebraic effects by concept? E.g. the io passed in is an effect handler, and it is the effect handler's choice whether to perform stack switching (or other means of non-blocking waiting) to enable asynchronicity?
wucke13
·작년·discuss
This seems to go into a similar direction like ZeroTier, but actually open source. There is almost no discussion of this in the western hemisphere, but I'd be interested what people think about it.
wucke13
·작년·discuss
When I first read the examples, besides my laughter, I felt a similar disconnect im the semantics of the chosen German words. Thank you for you suggestions, I agree with all of them, they are better indeed IMHO.
wucke13
·작년·discuss
I think ZMK (available on the Nice!Nano) does exactly that already?
wucke13
·작년·discuss
Would the Paris Climate Agreement not qualify as a treaty?
wucke13
·작년·discuss
Tangentially relevant: Gernots list of benchmarking crimes.

https://gernot-heiser.org/benchmarking-crimes.html