2021-06-27 04:34:21 <neuro_      > Why does this result in Stack overflow in gforth: 1000 allot here sp!
2021-06-27 04:34:54 <neuro_      > Ah because it messes up with the text interpreter's stack state right?
2021-06-27 04:36:31 <neuro_      > Indeed changing it inside compiled code and restoring before exit has no problem
2021-06-27 09:32:20 <veltas      > neuro_: No it's a stack overflow because you set the stack pointer to somewhere totally different, and the stack overflow check is just to make sure the pointer is in an appropriate range
2021-06-27 09:32:45 <veltas      > And the stack overflow check is usually only done at the interpreter loop, so in a compiled code it would not get checked before being restored again
2021-06-27 09:34:22 <veltas      > The interpreter loop is designed to handle the stack being changed, but not the return stack. But it can't handle the stack being moved apparently.
2021-06-27 12:20:04 <KipIngram   > That's right (what veltas said).  It check stack bounds in between word interpretations.  When you compile the change and the restore inside a word, no check is performed before you restore it.
2021-06-27 12:20:44 <siraben     > remexre: I wrote a new blog post https://siraben.github.io/2021/06/27/classical-math-coq.html
2021-06-27 12:20:54 <KipIngram   > You might try including a suitable update to sp0 as well.
2021-06-27 12:21:12 <KipIngram   > The stack check is to compare the stack pointer to the value in sp0.  If you change them both, you may be fine.
2021-06-27 12:21:36 <KipIngram   > sp0 is just a variable that holds the address of the "bottom" of the stack.
2021-06-27 12:21:49 <KipIngram   > It's what the stack pointer should be when the stack is empty.
2021-06-27 12:23:05 <KipIngram   > Here:
2021-06-27 12:23:08 <KipIngram   > Gforth 0.7.3, Copyright (C) 1995-2008 Free Software Foundation, Inc.
2021-06-27 12:23:10 <KipIngram   > Gforth comes with ABSOLUTELY NO WARRANTY; for details type `license'
2021-06-27 12:23:12 <KipIngram   > Type `bye' to exit
2021-06-27 12:23:14 <KipIngram   > : newstack 1000 allot here sp0 ! here sp! ;  ok
2021-06-27 12:23:16 <KipIngram   > newstack  ok
2021-06-27 12:23:18 <KipIngram   >   ok
2021-06-27 12:23:20 <KipIngram   >   ok
2021-06-27 12:23:38 <KipIngram   > sp@ here - . 0  ok
2021-06-27 12:24:49 <KipIngram   > That seems to work.
2021-06-27 12:26:43 <KipIngram   > I would imagine you could do the return stack as well, but it would be more delicate.  You'd need to copy over the return addresses on the stack required to get you back to the interpreter.  That would
2021-06-27 12:26:47 <KipIngram   > Or something like that at least.
2021-06-27 12:27:01 <KipIngram   > Or you could do the update and then run QUIT.
2021-06-27 12:27:46 <KipIngram   > This also seems to work:
2021-06-27 12:27:59 <KipIngram   > : newreturnstack  1000 allot here rp0 ! here rp! quit ;
2021-06-27 12:28:33 <KipIngram   > QUIT abandons the extant return stack and clears it (rp0 @ rp!) and re-enters the outer interpreter.
2021-06-27 12:30:01 <KipIngram   > If I run newreturnstack and then do rp@ here - I get -128.  So the interpreter loop has quite a few entries on the return stack already, apparently.
2021-06-27 12:31:57 <KipIngram   > So, long story short, the system knows where *both ends* of each stack is.  To move the stack you have to change both of those things.
2021-06-27 12:32:10 <KipIngram   > both ends "are"
2021-06-27 14:15:29 <eris[m]12   > oh hey, crc runs this channel!
2021-06-27 14:15:54 <eris[m]12   > nice work on retroforth!
2021-06-27 14:16:06 <remexre     > siraben: huh, neat; I haven't seen sumor before, makes sense that something like it would exist
2021-06-27 14:16:27 <eris[m]12   > its nice to see interesting stuff in the forth space
2021-06-27 14:19:38 <crc         > eris[m]12: thanks, and welcome to the channel
2021-06-27 14:21:12 <Mat9        > G'Day. May I ask what sumor is?
2021-06-27 14:21:22 <eris[m]12   > ^^
2021-06-27 14:22:20 <crc         > Mat9: see https://siraben.github.io/2021/06/27/classical-math-coq.html
2021-06-27 14:22:35 <Mat9        > thanks
2021-06-27 14:26:20 <KipIngram   > I find all that stuff siraben et al dwell on to be absolutely fascinting, and yet also completely outside my wheelhouse.  Far enough outside that I thing quite a bit of effort would be involved in becom
2021-06-27 14:26:46 <KipIngram   > I sort of think of it as the "theoretical side" of math.
2021-06-27 14:27:01 <KipIngram   > I quite like theory in science, but I've never really delved deeply into that sort of thing on the math side.
2021-06-27 14:27:20 <KipIngram   > But I'm happy people are out there dealing with it.  :-)
2021-06-27 14:31:34 <Mat9        > I'm not sure what he inteded with his analysis but it would be probably helpful for checking program correctness
2021-06-27 14:34:58 <Mat9        > ok, seems he is interrested in computer assisted theorem proving
2021-06-27 15:36:42 <KipIngram   > Yes, right - correctness proof is a core of his interests.
2021-06-27 15:37:09 <KipIngram   > And I respect the value of that sort of thing, in spite of not really having an interest in doing all the work I'd need to do to manage it myself.
2021-06-27 15:37:35 <KipIngram   > Lord knows there are enough bugs already - anything we can do to prevent / contain more of them is a good thing.
2021-06-27 16:52:42 <neuro_      > Writing Forth code in assembler by hand compiling it without a REPL. It's already comfortable enough.
2021-06-27 17:31:45 <moon        > I should write my own FORTH for P2
2021-06-27 17:31:59 <moon        > i have a clever idea for making stack a bit faster
2021-06-27 17:32:03 <eris[m]12   > P2?
2021-06-27 17:32:07 <moon        > Propeller 2
2021-06-27 17:32:38 <eris[m]12   > ah!
2021-06-27 17:32:42 <moon        > the existing TAQOZ FORTH is great, but it's Propeller 1 optimized in places still
2021-06-27 17:32:52 <eris[m]12   > do tell the ideas!
2021-06-27 17:33:27 <moon        > Well, the system supports indirect access to it's (massive 496 longword) register file
2021-06-27 17:33:44 <eris[m]12   > i kbow nothing of the propeller 2 other than the grotesque register count
2021-06-27 17:33:44 <moon        > so it's optimal to put the stack entirely inside the system regfile
2021-06-27 17:33:51 <eris[m]12   > how many bytes is a longword?
2021-06-27 17:33:54 <moon        > 4
2021-06-27 17:33:58 <eris[m]12   > ah
2021-06-27 17:34:16 <eris[m]12   > thats...
2021-06-27 17:34:20 <eris[m]12   > more than i thought it had
2021-06-27 17:34:38 <moon        > TAQOZ puts the stack in the local memory, but it's LUTRAM (512 x 32 bit as well, but not direct access like the regfile)
2021-06-27 17:34:47 <moon        > so it still has to cache the TOS
2021-06-27 17:35:00 <moon        > this gives better perf for words that don't push/drop, but worse for those that do
2021-06-27 17:35:24 <moon        > as when they do it has to adjust it's 4 entry cache as you'd expect
2021-06-27 17:35:56 <moon        > it also leaves most of LUTRAM unused which is :(
2021-06-27 17:36:50 <moon        > putting it in the regfile and using indirection improves the perf of words that push/drop (No more cache juggling) and slightly worsens those that don't
2021-06-27 17:37:14 <moon        > it's tradeoffs really
2021-06-27 17:38:19 <moon        > i still need to bench it, but i think overall perf would improve a bit, in exchange for worsening in code that never changes the TOS pointer
2021-06-27 17:40:10 <moon        > eris[m]12> i kbow nothing of the propeller 2 other than the grotesque register count | Also it's a really nice MCU, just.. needs better tooling ^^;
2021-06-27 17:40:32 <moon        > full GCC/Clang support isn't there
2021-06-27 17:47:06 <dave0       > maw
2021-06-27 18:06:33 <eris[m]12   > <moon "eris> i kbow nothing of the prop"> thats good to hear
2021-06-27 18:36:29 <cbridge     > <cmtptr> ptoooooooo
2021-06-27 18:36:47 <cbridge     > <cmtptr> all next week
2021-06-27 18:37:03 <cbridge     > <cmtptr> have fun working, suckers!
2021-06-27 18:46:24 <tabemann    > I have the weirdest problem
2021-06-27 18:46:55 <tabemann    > I revised my DO/?DO/LOOP/+LOOP/I/J/LEAVE/UNLOOP to be written in assembly
2021-06-27 18:47:35 <tabemann    > and now the return stack and occasionally the data stack are being corrupted randomly
2021-06-27 18:48:13 <tabemann    > switching the code to use the default systick handler rather than the task systick handler makes the problem go away most of the time, but not all of the time
2021-06-27 18:49:57 <mecrisp     > Does it work flawless if you disable interrupts completely?
2021-06-27 18:50:03 <tabemann    > nope
2021-06-27 18:50:48 <mecrisp     > Is count and limit on stack, or in dedicated registers?
2021-06-27 18:51:01 <tabemann    > count and limit on the rstack
2021-06-27 18:51:09 <tabemann    > leave address is also on the rstack
2021-06-27 18:51:30 <NieDzejkob  > are the implementations compatible enough to take half of the words from the asm impl and half from the previous forth impl?
2021-06-27 18:51:34 <moon        > what does the corruption tend to look like? Can't help much more without code though
2021-06-27 18:51:43 <mecrisp     > Then it may be sensitive to the way you compile the primitives - maybe you can break it by mixing postpone in
2021-06-27 18:52:02 <tabemann    > moon example is this:
2021-06-27 18:52:03 <NieDzejkob  > i.e. bisect the problem down to a single word
2021-06-27 18:52:19 <moon        > yea if at all possible it'd be best to bisect
2021-06-27 18:52:59 <tabemann    > : foo 0 over 16 + rot do false or loop ;
2021-06-27 18:53:18 <tabemann    > this word originally took an address but I rendered the address irrelevant
2021-06-27 18:53:31 <NieDzejkob  > my brain always page faults when reading code with ROT
2021-06-27 18:53:40 <tabemann    > usually it returns zero - very rarely it occasionally returns non-zero
2021-06-27 18:54:26 <tabemann    > okay
2021-06-27 18:54:34 <NieDzejkob  > okay, got it now
2021-06-27 18:54:55 <mecrisp     > Could you please give a disassembler listing of FOO ?
2021-06-27 18:55:05 <NieDzejkob  > how can it be nondeterministic if interrupts are disabled?
2021-06-27 18:56:56 <moon        > NMI?
2021-06-27 18:57:00 <tabemann    > well wtff
2021-06-27 18:57:08 <tabemann    > I just decompiled FOO
2021-06-27 18:57:19 <tabemann    > and it's not compiling BLX instructions
2021-06-27 18:57:24 <moon        > ow
2021-06-27 18:57:40 <mecrisp     > Sometimes explaining the problem solves it :-)
2021-06-27 18:57:47 <mecrisp     > Travis, have fun!
2021-06-27 18:58:09 <mecrisp     > And always disassembler definitions with strange behaviour as long as your compiler is unstable.
2021-06-27 18:58:53 <tabemann    > actually, I'm wrong
2021-06-27 18:59:05 <tabemann    > those are addresses being passed into DO and LOOP
2021-06-27 18:59:15 <tabemann    > they're correct
2021-06-27 19:01:37 <tabemann    > I'd forgotten that DO and LOOP both take an extra argument, the former being a LEAVE address to be put on the rstack and the latter being an address to jump to
2021-06-27 19:04:29 <tabemann    > okay, I just tried something
2021-06-27 19:04:49 <tabemann    > wait a sec that wouldn't work
2021-06-27 19:06:27 <tabemann    > okay, I tried it again the right way this time
2021-06-27 19:06:37 <tabemann    > I set the VTOI to $00200000
2021-06-27 19:07:17 <NieDzejkob  > what arch is your forth running on?
2021-06-27 19:07:27 <tabemann    > to effectively turn off all interrupt handling, without turning off all interrupts (which is infeable in zeptoforth in practice, as there is a variety of code that turns int
2021-06-27 19:07:48 <tabemann    > right now I'm running on Cortex-M7, specificially STM32F746
2021-06-27 19:08:00 <tabemann    > anyways, it works when I do this
2021-06-27 19:09:08 <NieDzejkob  > does your implementation use any variables? perhaps it's non-reentrant
2021-06-27 19:09:22 <NieDzejkob  > do your interrupt handlers use do-loops?
2021-06-27 19:09:44 <tabemann    > my LOOP implementation does not use variables
2021-06-27 19:10:17 <tabemann    > I'd have to check to make sure my interrupt handlers don't use do-loops, but I don't think it'd be relevant
2021-06-27 19:11:54 <tabemann    > also, my LOOP counter and end are stored on the rstack, not in registers
2021-06-27 19:12:05 <NieDzejkob  > okay, maybe add some assembly code at the beginning of your interrupt handler that saves the address of the code it interrupted in a global variable
2021-06-27 19:12:27 <NieDzejkob  > and then inside your test loop, as soon as your state gets corrupted, read that global and print it
2021-06-27 19:14:06 <tabemann    > I know what code is being interrupted, that's the thing
2021-06-27 19:14:32 <tabemann    > my big question is why is it corrupting it very infrequently
2021-06-27 19:16:08 <NieDzejkob  > well maybe it only happens during a 2-instruction window
2021-06-27 19:16:25 <tabemann    > and also, it's corrupting both the data stack and the rstack
2021-06-27 19:16:45 <tabemann    > which makes me think it's actually corrupting registers, not memory
2021-06-27 19:16:57 <NieDzejkob  > do interrupts run on their own stacks?
2021-06-27 19:17:03 <tabemann    > nope
2021-06-27 19:17:52 <NieDzejkob  > perhaps there's a moment where a stack read or write is incomplete, so the interrupts overwrite the top slot?
2021-06-27 19:18:18 <NieDzejkob  > did you post your implementation of the relevant words here yet?
2021-06-27 19:18:27 <tabemann    > IIRC aligned word accesses are atomic
2021-06-27 19:18:36 <tabemann    > nope
2021-06-27 19:19:03 <NieDzejkob  > any reason not to?
2021-06-27 19:20:29 <tabemann    > https://dpaste.org/dmFj#L
2021-06-27 19:22:16 <tabemann    > https://dpaste.org/4kXr
2021-06-27 19:24:03 <tabemann    > I didn't realize there's both a dpaste.org and dpaste.com...
2021-06-27 19:24:55 <tabemann    > anyways
2021-06-27 19:28:05 <tabemann    > to me nothing unkosher looks to be case with that code
2021-06-27 19:31:29 <tabemann    > I just checked to make sure the non-FP exception frame format is the same on the M7 and the M4, and this is the case
2021-06-27 19:33:44 <NieDzejkob  > what's the purpose of the 6?
2021-06-27 19:36:06 <tabemann    > R6
2021-06-27 19:36:34 <tabemann    > it's compiling a group of instructions to set the value of R6 to a constant
2021-06-27 19:37:28 <NieDzejkob  > tos = r6?
2021-06-27 19:39:16 <tabemann    > yep
2021-06-27 19:44:20 <tabemann    > I'm trying to think of how an interrupt handler could be causing corruption of both the rstack and dstack - note that the only registers used internally by words which are n
2021-06-27 19:45:05 <tabemann    > bbl
2021-06-27 20:07:24 <tabemann    > back
2021-06-27 22:08:18 <siraben     > Mat9: the post was just about some surprising things that happen when one translate classical mathematics into a constructive setting
2021-06-27 22:08:44 <siraben     > for CS and program verification, there isn't much of an issue because CS is almost all constructive anyway
2021-06-27 22:10:00 <siraben     > Here's a more forth related thing, https://gist.github.com/siraben/4361eca01cb0395cfa3c993e0dd380f3 I wrote up a formal semantics for a subset of Forth, just to play around
2021-06-27 22:10:35 <siraben     > factorial defined as: 1 begin over O= not while factorial_body repeat swap drop
2021-06-27 22:10:56 <siraben     > s/translate/translates
2021-06-27 22:14:23 <moon        > Coq is waaaay over my head
2021-06-27 22:14:30 <moon        > but neat
2021-06-27 22:20:54 <siraben     > remexre: "Typed programs don't leak data" https://dodisturb.me/posts/2021-06-27-Typed-Programs-Dont-Leak-Data.html
2021-06-27 22:22:02 <siraben     > And using the right framework, you can prove real programs (e.g. written in C) correct https://gist.github.com/siraben/bdc2aa9b4a8f197722411b334febeaa0