nexgen2 has quit [Remote host closed the connection]
nexgen2 has joined #riscv
nexgen2 has quit [Remote host closed the connection]
nexgen2 has joined #riscv
somlo has quit [Remote host closed the connection]
somlo has joined #riscv
jacklsw has joined #riscv
vagrantc has joined #riscv
jmdaemon has joined #riscv
frost has joined #riscv
vagrantc has quit [Quit: leaving]
jmdaemon has quit [Quit: WeeChat 3.3]
jmd has joined #riscv
jmd has quit [Client Quit]
jmdaemon has joined #riscv
jmdaemon has quit [Client Quit]
jmdaemon has joined #riscv
jmdaemon has quit [Client Quit]
jmdaemon has joined #riscv
rlittl01 has joined #riscv
jmdaemon has quit [Ping timeout: 252 seconds]
mahmutov has quit [Ping timeout: 250 seconds]
PyroPeter has quit [Ping timeout: 250 seconds]
PyroPeter has joined #riscv
jmdaemon has joined #riscv
cwebber has joined #riscv
arandomcomrade has joined #riscv
davidlt has joined #riscv
wgrant has quit [Quit: WeeChat 2.8]
frost has quit [Remote host closed the connection]
riff-IRC has quit [Remote host closed the connection]
frost has joined #riscv
riff-IRC has joined #riscv
arandomcomrade has quit [Quit: Leaving]
jmdaemon has quit [Ping timeout: 250 seconds]
wgrant has joined #riscv
BOKALDO has joined #riscv
MichaelZhu has joined #riscv
jmdaemon has joined #riscv
davidlt has quit [Ping timeout: 250 seconds]
MichaelZhu has quit [Remote host closed the connection]
abelvesa has quit [Quit: leaving]
abelvesa has joined #riscv
MichaelZhu has joined #riscv
EchelonX has quit [Quit: Leaving]
frost has quit [Ping timeout: 256 seconds]
mahmutov has joined #riscv
<gordonDrogon>
Esmil, Thanks. The K210 looks nice but it's got the same/similar issues of a few other RV platforms (from my point of view) in that it's "too much". dual-core 64-bit plus all the image and AI stuff - I also can't find a simple spec. for how much RAM and Flash it has (not that unusual either - but why?)
<gordonDrogon>
but yes, the 'retrocomputing' thing is a weird thing in itself. I started computing in '78 on the Apple II, so my own view is probably highly biased with that, although I dabbled in the dec pdp8 and 11 world for some time too.
aburgess has quit [Ping timeout: 252 seconds]
peeps has quit [Remote host closed the connection]
peeps has joined #riscv
jjido has joined #riscv
rlittl01 has quit [Remote host closed the connection]
aburgess has joined #riscv
peeps[zen] has joined #riscv
peeps has quit [Ping timeout: 252 seconds]
smartin has joined #riscv
peepsalot has joined #riscv
peeps[zen] has quit [Ping timeout: 256 seconds]
MichaelZhu has quit [Remote host closed the connection]
pecastro has joined #riscv
davidlt has joined #riscv
<Sofia>
Hmm. Reading over the spec. I'm wondering how often, if ever, the MULHSU is actually ever used? I expect rarely because it basically requires a language which lets you write signed * unsigned integers (I'm going to call that too few...), or the manual invocation of the specific intrinsic. I added binutils to my alpine risc-v qemu chroot to objdump all the very few binaries I have at my fingertips.
<Sofia>
I don't get ANY instances of the instruction.
<Sofia>
Without casting to one or the other incorrectly. **
<Sofia>
Searching for mulh, I only get mulhu and clmulh (and this one requires the bitmanip extension!)
<Sofia>
Language accessibility aside; more importantly it'd need even a use.
aburgess has quit [Ping timeout: 250 seconds]
mahmutov has quit [Ping timeout: 252 seconds]
jjido has quit [Quit: My MacBook Air has gone to sleep. ZZZzzz…]
winterflaw has joined #riscv
jmdaemon has quit [Quit: WeeChat 3.3]
FL4SHK has quit [Ping timeout: 252 seconds]
FL4SHK has joined #riscv
MichaelZhu has joined #riscv
MichaelZhu has quit [Remote host closed the connection]
MichaelZhu has joined #riscv
MichaelZhu has quit [Remote host closed the connection]
MichaelZhu has joined #riscv
MichaelZhu has quit [Remote host closed the connection]
MichaelZhu has joined #riscv
aburgess has joined #riscv
Andre_H has joined #riscv
BOKALDO has quit [Quit: Leaving]
\dev\ice has quit [Ping timeout: 250 seconds]
<muurkha>
Sofia: hmm, don't you need it for multiple-precision multiply?
<muurkha>
23:06 < dh`> that was a decade in which things changed a lot faster than anytime recently
<muurkha>
it is probably not a coincidence that at the end of that decade software became copyrightable, and a few years later patentable
MichaelZhu has quit [Remote host closed the connection]
MichaelZhu has joined #riscv
mahmutov has joined #riscv
<Sofia>
muurkha: Although not for multi, at least u64,u64 -> u128 and i64,i64 -> i128 are mulhu and mulh respectively. But neither are mulhsu.
<muurkha>
well, I was thinking like i4096 × i4096
voltron has joined #riscv
<Sofia>
Then I don't know.
<muurkha>
well, I haven't actually implemented it myself
<muurkha>
and I guess it's really things like i128 × i128 where it would really matter
<Sofia>
When I work with large numbers, I use reduced radix representations and never needed such an intrinsic.
MichaelZhu has quit [Ping timeout: 252 seconds]
<muurkha>
you mean, like half a machine word per limb instead of a whole machine word?
<muurkha>
if you want to compute (2⁶⁴a + b) × (2⁶⁴c + d) where a and c are signed and b and d are unsigned, as would be normal in two's-complement
<muurkha>
yeah, but it's still three muls and a mulhu
<muurkha>
can't argue that C types aren't a nightmare. they look simple but there's a congeries of teeming bugs just under the surface
<Sofia>
And two adds, yeah.
<muurkha>
right
stefanct has joined #riscv
<Sofia>
I find very few languages to have reasonable types. Play with dependently typed languages and the rest become annoyingly primitive. :P
<muurkha>
haha
MichaelZhu has quit [Ping timeout: 256 seconds]
<muurkha>
careful with the decidability there!
MichaelZhu has joined #riscv
* Sofia
is writing her assembler in Lean 4, a general purpose / theorem prover with dependent types. ^
MichaelZhu has quit [Remote host closed the connection]
<muurkha>
LEAN looks pretty appealing to me. what do you think of coqasm?
MichaelZhu has joined #riscv
<muurkha>
pardon me, L∃∀N
MichaelZhu has quit [Remote host closed the connection]
<Sofia>
Recently back to the drawing board to consider different approaches to encode it all, along with the properties that I care about. I basically want a memory safe constrained abstract machine, which I can compile to at least RISC-V and WebAssembly targets.
<Sofia>
Just Lean, heh.
<Sofia>
I do'nt know coqasm
<Sofia>
don't*
MichaelZhu has joined #riscv
<muurkha>
coqasm.pdf
MichaelZhu has quit [Remote host closed the connection]
<muurkha>
that sounds pretty desirable. what's your approach to representing pointers?
MichaelZhu has joined #riscv
<muurkha>
I feel uncomfortably out of my depth with provers in general, which I think is a sign I should spend more time with them
MichaelZhu has quit [Remote host closed the connection]
MichaelZhu has joined #riscv
<muurkha>
yeah, that one
davidlt has quit [Ping timeout: 252 seconds]
MichaelZhu has quit [Remote host closed the connection]
<muurkha>
oh, I know what we were doing wrong with the multi-precision stuff
<muurkha>
we're only taking the low 128 bits of the result
<Sofia>
As for pointers, not yet decided exactly. But plausibly by saturating either to the exact bounds or to +/- 1 as a sentinel, with implicit checks which branch to illegal instructions. At least in the lazy case, in the less lazy case, I'd require bounds proofs to lift the injection.
<muurkha>
unfortunately rv32gc gcc doesn't support __int128
<Sofia>
Ideally you can specify your program with as many extensions as you like; and the compiler will rewrite as necessary for your target subset. Or vice versa, spec low and optimize for better utilization.
<gordonDrogon>
BCPL has a 'muldiv' function... result := muldiv (a,b,c) where it's a*b / c and a*b is evaluated to 64-bits internally (for 32-bit a and b). It's designed for scaled arithmetic. It's all signed too
<muurkha>
so you're representing pointers as (segment, offset) pairs, where the segment either is or refers to a (base, bound) pair?
<gordonDrogon>
BCPL types aren't a nightmare - mostly because there aren't any ;-)
<muurkha>
gordonDrogon: yeah, Forth has that too
<muurkha>
I guess the main thing I'm wondering about is how you're handling the typing of the pointers. can you store them in memory that is sometimes used to store integers?
<Sofia>
This means forbiding syscalls, CSRs, arbitrary control flow and arbitrary pointer arithmetic. Use an unsafe extension which disables any optimizations which need to rely on the safety over the respective terms (unless you prove your unsafe code meets the safety criteria to re-enable the affected optimizations)
stefanct has quit [Ping timeout: 240 seconds]
<muurkha>
sure, that's reasonable
<Sofia>
muurkha: Not sure which "segment" you mean, but I was thinking a "divisible chunk of memory" where the address cannot be observed (or can be observed only if the dataflow does not leak the observation to the result of the program. I.e. can influence the computation but not the result)
<muurkha>
by "segment" I just meant a (base, bound) pair, or something analogous
<muurkha>
so if you want to compose safety proofs of different subroutines, you need lemmas that say a given subroutine never observes a given input, except to use it to index memory?
<muurkha>
somewhat analogous to treating it as an object reference in the JVM
<Sofia>
Ignoring the plausible saturating detail. The important detail is only that __whatever you do to the pointer__ is either allowed where reads outside your range assume a defined default (alternatively an illegal instruction, depends if you care). The important detail here is confidentiality and integrity, you may not observe values you should not see, nor should you taint any you should not be able
<Sofia>
to write to. The semantic difference of assuming a zero read (or other default) vs. crashing the program should be chosen by the programmer.
<Sofia>
Similar to how Lean defines division by zero, as returning zero. Or RISC-V defines it as -1.
<muurkha>
sure
<muurkha>
I'm just wondering how you handle storing pointers in memory
<muurkha>
I mean, there exist different alternatives, I'm not saying it's an insoluble problem
voltron has quit [Remote host closed the connection]
<Sofia>
I think the best option would be to set a dirty flag and assume a static zero read (or other read which causes termination). If the dirty flag is set, you know the result is incorrect, but you don't need to break the computation. An optimistic exception, assuming it almost never hits while detecting it and minimizing panic-branch bloat..
<muurkha>
Lean doesn't set a dirty flag on division by zero, though
<muurkha>
it's just that usually you need to prove that your divisor isn't zero
<Sofia>
It doesn't need to. If you want to prove something, and even prove it true for their defined value of division by zero, that is fine. You just might have proven something you didn't mean to prove. Usually you'd guard your proofs, not the evaluation. If your proof requires a non-zero input proof, then your proof doesn't need to even know the definition of division by zero.
<muurkha>
right, exactly. and you could use the same approach for examining pointer bits
<Sofia>
I know Lean 4 allows you to inject assertions. There are details there which that does. I'm not entirely sure what it does. Either way, I'd rather a dirty bit to capture the event without forcing control flow down a panic-style branch. I want to know the incorrect result, and why it was incorrect, so I can fix it.
jack_lsw has joined #riscv
<muurkha>
It'll be interesting to see what you come up with! I have in mind a similar project with slightly different objectives
<Sofia>
Please elaborate :)
<muurkha>
well, what I'm interested in is bootstrapping, and in particular bootstrapping reproducible computation
jacklsw has quit [Ping timeout: 260 seconds]
<muurkha>
if you come across some paper from 01892 that says "by summing the first five terms of the Taylor series rounded to 5 places we can calculate that sin(0.1) is about 0.09983", you can straightforwardly reproduce that computation and discover that they got it right
<muurkha>
or maybe that they got it wrong and it's actually 0.09982
<muurkha>
either way, it's an objective, falsifiable statement
<Sofia>
My target domains are: cryptography and graphics. The former is very sensitive to information leakage from the choice of program extraction, while the latter is very flexible in accepting bounded approximations.
<muurkha>
but if you come across a paper from 01992 that says "according to EISPACK the first eigenvalue of this matrix is 0.9512, so such and such a process is stable", you can't reproduce that
<muurkha>
maybe you run EISPACK and you get 1.0133. does that mean the original paper was wrong? not necessarily!
<Sofia>
In both cases I want to separate computation from representation, and a la Herbie (and its extension pherbie) to minimize error and latency. While constraining the output for data classification (crypto secret keys) and to bound the approximations.
stefanct has joined #riscv
voltron has joined #riscv
<muurkha>
you're using a different version of EISPACK, compiled with different compilers, running on different hardware implementing a different architecture, with different compiler options
<muurkha>
so it's totally expected that you'll get different results, unfortunately
<muurkha>
I think this is bad
Andre_H has quit [Quit: Leaving.]
<muurkha>
I mean, the natural sciences have been trundling along with that sort of reproducibility for centuries. it's totally reasonable to redo a physics experiment that reported a measurement of 0.9512 and get 1.0133, it probably just means your equipment is out of calibration or something
<muurkha>
but computation is math, we can aspire to bitwise reproducibility, as we do in cryptography
jack_lsw has quit [Quit: Back to the real life]
<Sofia>
I like how you prefix your years with an extra zero to indicate that we're already talking +8k years from now in the reproducibility request. :)
jacklsw has joined #riscv
<Sofia>
s/+/~/
<muurkha>
Exactly :)
<Sofia>
What you've described should be the baseline for all compilers and runtimes IMHO.
<muurkha>
it's likely that in 8000 years, or even in 80 years, it will be infeasible to dig up the version of GCC I used this year
<muurkha>
Well, it conflicts rather sharply with efficiency. For example, I think you probably can't use hardware floating point because it's probably buggy
<Sofia>
FWIW my plans should meet what you want, down to explicit bounds on the result due to the choice of precision of each input and intermediate value. I suspect you'd like pherbie. ;)
<muurkha>
"Fast Ray Tracing of Arbitrary Implicit Surfaces with Interval and Affine Arithmetic"
<muurkha>
what I mean is that "0.9512 ± 0.1" is not bitwise identical to "0.9512 ± 0.05"
<muurkha>
*graphics
<Sofia>
The bounded-error part is: if you have a computation you cannot evaluate in finite time because real numbers are a pain... then you can still bound the error and know your first 5 terms of the Taylor series, with 128-bit floating point precision (or 128-bit floating "bar" precision; an underspecified/incomplete format I'd like to experiment with).
<muurkha>
there's a whole bunch of work (which you might actually be more familiar with than I am) on accelerating ray tracing with variations of interval arithmetic
<muurkha>
especially for animations
<Sofia>
Unfortunately implemented in C++/CUDA and tied to nvidia, which I don't have, nor support.
<muurkha>
yeah, that's definitely in the same line of work
<muurkha>
reducing the expressions themselves is a really interesting approach! I'd never thought of that
jmdaemon has joined #riscv
<Sofia>
I don't plan to do ray tracing specifically. I want to optimize the derivation of an N-dimensionally defined implicit surface with bounded delta between frames to amortize the geometry processing to what could occur in successive frames. I.e. Animations follow deterministic paths and a human can only move their camera so far per frame without teleporting. If they teleport, then we deserve more time
<Sofia>
to evaluate the scene anyway.
<Sofia>
So yeah, I'm certainly working with interval arithmetic and I have variants of affine arithmetic waiting in the future for me to catch up first. :)
<muurkha>
right, exactly!
<Sofia>
I have a lot of optimization search space to play with. :)
jmdaemon has quit [Client Quit]
<muurkha>
I think, though I should emphasize that this is not based on actual experience or proofs, that for regular functions affine arithmetic, even RAA, should have much better scaling properties than ordinary interval arithmetic
<Sofia>
Taichi separates computation from representation; in the sense that you define your computations against a dense representation. And independently you may quickly iterate between many sparse representations, changing a line or two at a time for massive differences. The compiler does its analysis and further optimizes with some very nice tricks.
<Sofia>
That is not my project, no. That is Python and C++. I don't write either. :)
<muurkha>
haha
<Sofia>
DiffTaichi brings derivatives. :)
<muurkha>
right, that's the part I find most exciting actually
<Sofia>
QuantTaichi enables you to experiment with adjusting the precision of your types. Set your baseline with f64? See how changing to f32 or f16 or some custom fixed12, or whatever goes for each variable.
<muurkha>
(I mean of course linear functions are approximated perfectly by RAA and imperfectly with interval arithmetic, but even if your function looks quadratic locally, linear approximations can provide tighter error bounds to an arbitrarily high degree unless you're near a stationary point)
<Sofia>
But they don't automate any of this search. Whereas Pherbie does.
<muurkha>
I clearly have a lot of reading to do :)
<Sofia>
Pherbie doesn't automate the search by eye-ball comparing the results, it compares the error at each step of the computation.
<muurkha>
What do you think about modal interval arithmetic? I haven't managed to make heads or tails of it yet
<Sofia>
muurkha: Enjoyed the chat. But it is ... 315.
<muurkha>
oh, good night!
<Sofia>
I have not heard of this term.
<Sofia>
Feel free to leave paper links. :)
<Sofia>
Or maybe we should move to a /query? Kinda went offtopic. :)
<Sofia>
Did I mention that I want to measure my optimizing graphics compiler by cycle accurate RISC-V cost functions aware of pipelining details? Who needs to run things on GPUs or outside of virtual machines... Hey, if it amortizes enough of the computation, it might even work realtime under qemu. I can only hope.. :D
<muurkha>
haha, I guess modal interval arithmetic is not very related to the RISC-V ISA, is it?
<muurkha>
I was astounded to realize that computers are so fast I can now do real-time raytracing in Lua
<muurkha>
raymarching an implicit surface with an SDF
<Sofia>
Fortunately I'm not after ray tracing renders. But I do want global illumination.
<Sofia>
Caustics and glints sure are pretty, they are not on my roadmap.
davidlt has joined #riscv
<Sofia>
muurkha: Where ray marching evaluates the SDF multiple times per pixels. The interval subdivision of space evaluates the SDF only once per sub-region.
kailo has quit [Ping timeout: 256 seconds]
<perro>
muurkha when you say realtime you mean how fast?
<Sofia>
perro: 2.2 fps
<perro>
oh 2.2 fps
<Sofia>
That was the lua code at least.
<perro>
that is really impressive
<Sofia>
Says the line-1 comment
<Sofia>
muurkha: I wouldn't count that as realtime though. ;)
<Sofia>
At least it is in frames per second land and not hours per frame. :D
<Sofia>
Fair effort lua JIT (JIT yes..?)
* Sofia
is sleeping.. right? <_<
<Sofia>
TTYL o/
voltron has quit [Remote host closed the connection]
octav1a has joined #riscv
<octav1a>
yip
<sorear>
o/
<octav1a>
\o
jack_lsw has joined #riscv
jack_lsw has quit [Client Quit]
jacklsw has quit [Ping timeout: 268 seconds]
jack_lsw has joined #riscv
<muurkha>
yes! I agree that the speed lesaves something to be desired. and yes, LuaJIT
mahmutov has quit [Ping timeout: 256 seconds]
mahmutov has joined #riscv
elastic_dog has quit [Ping timeout: 265 seconds]
elastic_dog has joined #riscv
elastic_dog has quit [Client Quit]
elastic_dog has joined #riscv
jack_lsw has quit [Quit: Back to the real life]
llamp[m] has joined #riscv
voltron has joined #riscv
pecastro has quit [Ping timeout: 256 seconds]
pecastro has joined #riscv
stefanct has quit [Read error: Connection reset by peer]
stefanct has joined #riscv
jjido has joined #riscv
SpaceCoaster has quit [Quit: Bye]
SpaceCoaster has joined #riscv
DoubleJ has quit [Quit: I'll see you on the dark side of the moon]
DoubleJ has joined #riscv
BOKALDO has quit [Read error: Connection reset by peer]
davidlt has quit [Ping timeout: 252 seconds]
aburgess has quit [Remote host closed the connection]
aburgess has joined #riscv
freakazoid343 has joined #riscv
freakazoid12345 has quit [Ping timeout: 250 seconds]