matu3ba

6 ms·

1. 31.▲
   by matu3ba 1y ago

   Nice introduction. 1. Please always make closed and open interval explicit on all code examples. "Detecting overlap" is ambiguous and open intervals have no given solution in the article, if I'm not mistaken. 2. How do you de
2. 32.▲
   by matu3ba 1y ago

   Looks like a very reasonable guide for Python software debugging. Reversal computing/time reversal computing is missing, but probably Python programs are not that complex or long-running to use that. Does Python without GIL have valida
3. 33.▲
   by matu3ba 1y ago

   Please elaborate what "execution model" entails. What is the Rust "Abstract Machine"? I am only aware of the memory model, specifically pointer and consistency/synchronization which extends the C memory model by abs
4. 34.▲
   by matu3ba 1y ago

   Excellent news. Will be very interesting how the debugging experience will improve with scheduling, recording of io and reversal computing between io.
5. 35.▲
   by matu3ba 1y ago

   Yep, that would be more like structured concurrency also mentioned in linked blog post. sans-io is about state machine as interface, but unfortunately does not specify a formal model or how to synthesize/derive one etc.
6. 36.▲
   by matu3ba 1y ago

   Thanks for the info. Do you have a good overview on what other hardware properties or issues are relevant?
7. 37.▲
   by matu3ba 1y ago

   > LLVM will improve to the point that we don't need further annotation to enable positive optimization transformations That is quite a long way to go, since the following formal specs/models are missing to make LLVM + user conf
8. 38.▲
   by matu3ba 2y ago

   Would be very cool, if once finished, the techniques are applied to user-schedulable languages https://www.hytradboi.com/2025/7d2e91c8-aced-415d-b993-f6f85... . I guess they are too tailored to the actual memory layout
9. 39.▲
   by matu3ba 2y ago

   How does it compare to dinit, which is usable in Linuxes, BSDs and default used by Chimera Linux? The goals look identical, see Introduction at https://github.com/davmac314/dinit .
10. 40.▲
    by matu3ba 2y ago

    Thanks for the interesting insight. 1. What would you recommend to model multi-thread or multi-process problems on the same system? Is there a good read to give recommendations? 2. Is there a good overview on trade-offs between CSP, Actor m
11. 41.▲
    by matu3ba 2y ago

    "Diagrams are code" exists as ladder diagrams for PLC, from which Structured Text can be derived, which typically are used by PICs for simple to estimate time behavior in very time-sensitive/critical (real-time) control appli
12. 42.▲
    by matu3ba 2y ago

    A rewrite of such technologies would not fix their semantic problems and related architecture decisions around tractability, debugging etc. For example, rewriting LLVM and GCC does not fix the underlying problem of missing code semantics le
13. 43.▲
    by matu3ba 2y ago

    Example 1 is a deficit of C with missing computed goto and switch continue. Example 2 review is ambiguous on practicality. Example 3 reads very odd, an over-approximated upper stack bound is very possible https://github.com/
14. 44.▲
    by matu3ba 2y ago

    That looks very promising. Imagine development speed based on that and for Zig and 1. static analysis, 2. dynamic analysis, 3. debugging/introspection tooling (code reduction, io-substitution), 4. backend experimentation.
15. 45.▲
    by matu3ba 2y ago

    Yes, I do agree with you. Just wanted to inform you that it may still be possible in principle and as you can see with development speed, build system, dependencies etc there is a potential angle.
16. 46.▲
    by matu3ba 2y ago

    > We don't have a Rust-killer language yet. The type-system analysis of Rust is smart, but not restricted to the language per se, see https://github.com/ityonemo/clr . One merely has to have proper namespacing a
17. 47.▲
    by matu3ba 2y ago

    Looks like my definition of memory safety is wrong and it means only "Runtime makes sure incorrect memory reads/writes are not possible", not by what means, so crashing is under that definition ok.
18. 48.▲
    by matu3ba 2y ago

    If you have the data set of known bugs, going through them should give you the cause. I do expect a strong correlation of basic coverage for simple UB things and input set/formulae coverage for the harder to hit ones, specifically as t
19. 49.▲
    by matu3ba 2y ago

    Neither Rust is memory safe due to stackoverflow on recursion or in the call chain being possible. Sanitation is very much possible, so it is no design problem, see https://matu3ba.github.io/articles/optimal_debugging&#
20. 50.▲
    by matu3ba 2y ago

    What kind/class of issues are caused by "thread interleaving on the scale of nanoseconds"? Faulty CPU bit flips due to radiation/quantum effects or what are you referring to? Just curious.
21. 51.▲
    by matu3ba 2y ago

    Thanks for your write-up, this is very helpful for understanding.
22. 52.▲
    by matu3ba 2y ago

    Thanks for clarification. I have not been aware of thread fuzzing and chaos mode before.
23. 53.▲
    by matu3ba 2y ago

    So the only way to trace probe consumer desktop CPUs and possibly GPUs is by the hardware vendors them-self or specialized facilities/laboratories? For Intel I can find https://www.lauterbach.com/supported-platforms&#x2
24. 54.▲
    by matu3ba 2y ago

    windbg has no sane library api, which makes it by construction unsuitable for automation and inspection. I'd personally prefer, if we would have the options of multiple time-travel debugging sessions based on synchronization points (if
25. 55.▲
    by matu3ba 2y ago

    Are you aware of solutions for multi-threaded and relative time-accurate recordings, for example by using user-selected synchronization points? Afaiu, rr and undo do simulation of threads on one CPU core, which rules out detecting timing is
26. 56.▲
    by matu3ba 2y ago

    Hard mode Rust provides the trickyness of separating memory handling from the (pure) code logic https://matklad.github.io/2022/10/06/hard-mode-rust.html which makes batching inputs unnecessary hard. The other
27. 57.▲
    by matu3ba 3y ago

    My conclusion from this: There won't be a close-to-optimal ISA for high perf (big cores) in the near-to-mid future unless there is a completely new market creates demand. + Nobody bothers documenting publicly semantics and time informa
28. 58.▲
    by matu3ba 3y ago

    A more recent example of excellent work with Zig on improving state of the art parsing can be seen in this fine presentation of a SIMD-heavy project: https://www.youtube.com/watch?v=oN8LDpWuPWw . It shows SWAR-techiques for
29. 59.▲
    by matu3ba 3y ago

    Looking nice, I like the rationale. Some questions from my side: - 1. As far as I understand, there are multiple models for a linear type system. Which one does Austral implement? Is it verified to be correct? - 2. Since there is a static c
30. 60.▲
    by matu3ba 3y ago

    I know of TCF from https://www.cs.yale.edu/homes/antonopoulos-timos/PLDI-2017.p... , but the folks from sel4 have likely improved the models as they have a full research team on it: https://trustworthy.s