00:00:00 --- log: started forth/21.06.27
00:28:05 --- join: rain3 joined #forth
01:34:44 <cbridge_> <neuro_> Why does this result in Stack overflow in gforth: 1000 allot here sp!
01:35:18 <cbridge_> <neuro_> Ah because it messes up with the text interpreter's stack state right?
01:36:55 <cbridge_> <neuro_> Indeed changing it inside compiled code and restoring before exit has no problem
02:41:56 --- join: Glider_IRC__ joined #forth
02:44:48 --- quit: Glider_IRC_ (Ping timeout: 120 seconds)
06:32:44 <cbridge_> <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
06:33:09 <cbridge_> <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
06:34:45 <cbridge_> <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.
07:38:38 --- join: joanna_ joined #forth
07:43:33 --- quit: joanna_ (Ping timeout: 120 seconds)
08:52:24 --- quit: rain3 (Ping timeout: 120 seconds)
09:20:28 <cbridge_> <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.
09:21:07 <cbridge_> <siraben> remexre: I wrote a new blog post https://siraben.github.io/2021/06/27/classical-math-coq.html
09:21:18 <cbridge_> <KipIngram> You might try including a suitable update to sp0 as well.
09:21:36 <cbridge_> <KipIngram> The stack check is to compare the stack pointer to the value in sp0.  If you change them both, you may be fine.
09:22:00 <cbridge_> <KipIngram> sp0 is just a variable that holds the address of the "bottom" of the stack.
09:22:13 <cbridge_> <KipIngram> It's what the stack pointer should be when the stack is empty.
09:23:27 <cbridge_> <KipIngram> Here:
09:23:33 <cbridge_> <KipIngram> Gforth 0.7.3, Copyright (C) 1995-2008 Free Software Foundation, Inc.
09:23:33 <cbridge_> <KipIngram> Gforth comes with ABSOLUTELY NO WARRANTY; for details type `license'
09:23:36 <cbridge_> <KipIngram> Type `bye' to exit
09:23:38 <cbridge_> <KipIngram> : newstack 1000 allot here sp0 ! here sp! ;  ok
09:23:41 <cbridge_> <KipIngram> newstack  ok
09:23:41 <cbridge_> <KipIngram>   ok
09:23:43 <cbridge_> <KipIngram>   ok
09:24:02 <cbridge_> <KipIngram> sp@ here - . 0  ok
09:25:12 <cbridge_> <KipIngram> That seems to work.
09:27:07 <cbridge_> <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 be the range between rp0 @ and rp@, I guess.
09:27:10 <cbridge_> <KipIngram> Or something like that at least.
09:27:23 <cbridge_> <KipIngram> Or you could do the update and then run QUIT.
09:28:09 <cbridge_> <KipIngram> This also seems to work:
09:28:23 <cbridge_> <KipIngram> : newreturnstack  1000 allot here rp0 ! here rp! quit ;
09:28:55 <cbridge_> <KipIngram> QUIT abandons the extant return stack and clears it (rp0 @ rp!) and re-enters the outer interpreter.
09:30:26 <cbridge_> <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.
09:32:21 <cbridge_> <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.
09:32:35 <cbridge_> <KipIngram> both ends "are"
09:43:36 --- join: rain3 joined #forth
11:15:52 <cbridge_> <eris[m]12> oh hey, crc runs this channel!
11:16:19 <cbridge_> <eris[m]12> nice work on retroforth!
11:16:30 <cbridge_> <remexre> siraben: huh, neat; I haven't seen sumor before, makes sense that something like it would exist
11:16:52 <cbridge_> <eris[m]12> its nice to see interesting stuff in the forth space
11:20:01 <cbridge_> <crc> eris[m]12: thanks, and welcome to the channel
11:21:37 <cbridge_> <Mat9> G'Day. May I ask what sumor is?
11:21:45 <cbridge_> <eris[m]12> ^^
11:22:43 <cbridge_> <crc> Mat9: see https://siraben.github.io/2021/06/27/classical-math-coq.html
11:22:59 <cbridge_> <Mat9> thanks
11:26:45 <cbridge_> <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 becoming proficient with it.
11:27:10 <cbridge_> <KipIngram> I sort of think of it as the "theoretical side" of math.
11:27:26 <cbridge_> <KipIngram> I quite like theory in science, but I've never really delved deeply into that sort of thing on the math side.
11:27:43 <cbridge_> <KipIngram> But I'm happy people are out there dealing with it.  :-)
11:31:59 <cbridge_> <Mat9> I'm not sure what he inteded with his analysis but it would be probably helpful for checking program correctness
11:35:23 <cbridge_> <Mat9> ok, seems he is interrested in computer assisted theorem proving
12:34:53 --- quit: rain3 (Ping timeout: 120 seconds)
12:37:07 <cbridge_> <KipIngram> Yes, right - correctness proof is a core of his interests.
12:37:32 <cbridge_> <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.
12:37:58 <cbridge_> <KipIngram> Lord knows there are enough bugs already - anything we can do to prevent / contain more of them is a good thing.
13:37:44 --- join: joanna_ joined #forth
13:50:33 --- quit: joanna_ (Ping timeout: 120 seconds)
13:53:06 <cbridge_> <neuro_> Writing Forth code in assembler by hand compiling it without a REPL. It's already comfortable enough.
14:12:12 --- join: joanna_ joined #forth
14:16:39 --- quit: joanna_ (Ping timeout: 120 seconds)
14:27:03 --- join: joanna_ joined #forth
14:32:10 <cbridge_> <moon> I should write my own FORTH for P2
14:32:24 <cbridge_> <moon> i have a clever idea for making stack a bit faster
14:32:27 <cbridge_> <eris[m]12> P2?
14:32:30 <cbridge_> <moon> Propeller 2
14:33:03 <cbridge_> <eris[m]12> ah!
14:33:05 <cbridge_> <moon> the existing TAQOZ FORTH is great, but it's Propeller 1 optimized in places still
14:33:17 <cbridge_> <eris[m]12> do tell the ideas!
14:33:50 <cbridge_> <moon> Well, the system supports indirect access to it's (massive 496 longword) register file
14:34:07 <cbridge_> <eris[m]12> i kbow nothing of the propeller 2 other than the grotesque register count
14:34:07 <cbridge_> <moon> so it's optimal to put the stack entirely inside the system regfile
14:34:16 <cbridge_> <eris[m]12> how many bytes is a longword?
14:34:19 <cbridge_> <moon> 4
14:34:22 <cbridge_> <eris[m]12> ah
14:34:40 <cbridge_> <eris[m]12> thats...
14:34:42 <cbridge_> <eris[m]12> more than i thought it had
14:35:03 <cbridge_> <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)
14:35:12 <cbridge_> <moon> so it still has to cache the TOS
14:35:24 <cbridge_> <moon> this gives better perf for words that don't push/drop, but worse for those that do
14:35:48 <cbridge_> <moon> as when they do it has to adjust it's 4 entry cache as you'd expect
14:36:20 <cbridge_> <moon> it also leaves most of LUTRAM unused which is :(
14:37:14 <cbridge_> <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
14:37:38 <cbridge_> <moon> it's tradeoffs really
14:38:44 <cbridge_> <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
14:40:35 <cbridge_> <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 ^^;
14:40:56 <cbridge_> <moon> full GCC/Clang support isn't there
14:44:07 --- join: Glider_IRC_ joined #forth
14:44:49 --- quit: Glider_IRC__ (Ping timeout: 120 seconds)
14:47:31 <cbridge_> <dave0> maw
15:03:39 --- quit: joanna_ (Ping timeout: 120 seconds)
15:06:56 <cbridge_> <eris[m]12> <moon "eris> i kbow nothing of the prop"> thats good to hear
15:29:28 --- join: joanna_ joined #forth
15:36:49 <cmtptr> ptoooooooo
15:37:06 <cmtptr> all next week
15:37:21 <cmtptr> have fun working, suckers!
15:46:49 <cbridge_> <tabemann> I have the weirdest problem
15:47:20 <cbridge_> <tabemann> I revised my DO/?DO/LOOP/+LOOP/I/J/LEAVE/UNLOOP to be written in assembly
15:48:00 <cbridge_> <tabemann> and now the return stack and occasionally the data stack are being corrupted randomly
15:48:37 <cbridge_> <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
15:50:22 <cbridge_> <mecrisp> Does it work flawless if you disable interrupts completely?
15:50:26 <cbridge_> <tabemann> nope
15:51:14 <cbridge_> <mecrisp> Is count and limit on stack, or in dedicated registers?
15:51:26 <cbridge_> <tabemann> count and limit on the rstack
15:51:32 <cbridge_> <tabemann> leave address is also on the rstack
15:51:54 <cbridge_> <NieDzejkob> are the implementations compatible enough to take half of the words from the asm impl and half from the previous forth impl?
15:51:57 <cbridge_> <moon> what does the corruption tend to look like? Can't help much more without code though
15:52:07 <cbridge_> <mecrisp> Then it may be sensitive to the way you compile the primitives - maybe you can break it by mixing postpone in
15:52:25 <cbridge_> <tabemann> moon example is this:
15:52:26 <cbridge_> <NieDzejkob> i.e. bisect the problem down to a single word
15:52:44 <cbridge_> <moon> yea if at all possible it'd be best to bisect
15:53:25 <cbridge_> <tabemann> : foo 0 over 16 + rot do false or loop ;
15:53:44 <cbridge_> <tabemann> this word originally took an address but I rendered the address irrelevant
15:53:56 <cbridge_> <NieDzejkob> my brain always page faults when reading code with ROT
15:54:06 <cbridge_> <tabemann> usually it returns zero - very rarely it occasionally returns non-zero
15:54:50 <cbridge_> <tabemann> okay
15:54:59 <cbridge_> <NieDzejkob> okay, got it now
15:55:18 <cbridge_> <mecrisp> Could you please give a disassembler listing of FOO ?
15:55:31 <cbridge_> <NieDzejkob> how can it be nondeterministic if interrupts are disabled?
15:57:19 <cbridge_> <moon> NMI?
15:57:23 <cbridge_> <tabemann> well wtff
15:57:32 <cbridge_> <tabemann> I just decompiled FOO
15:57:42 <cbridge_> <tabemann> and it's not compiling BLX instructions
15:57:48 <cbridge_> <moon> ow
15:58:04 <cbridge_> <mecrisp> Sometimes explaining the problem solves it :-)
15:58:10 <cbridge_> <mecrisp> Travis, have fun!
15:58:33 <cbridge_> <mecrisp> And always disassembler definitions with strange behaviour as long as your compiler is unstable.
15:59:17 <cbridge_> <tabemann> actually, I'm wrong
15:59:30 <cbridge_> <tabemann> those are addresses being passed into DO and LOOP
15:59:39 <cbridge_> <tabemann> they're correct
16:02:00 <cbridge_> <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
16:04:54 <cbridge_> <tabemann> okay, I just tried something
16:05:13 <cbridge_> <tabemann> wait a sec that wouldn't work
16:06:53 <cbridge_> <tabemann> okay, I tried it again the right way this time
16:07:02 <cbridge_> <tabemann> I set the VTOI to $00200000
16:07:08 --- quit: joanna_ (Ping timeout: 120 seconds)
16:07:41 <cbridge_> <NieDzejkob> what arch is your forth running on?
16:07:51 <cbridge_> <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 interrupts on and off)
16:08:10 <cbridge_> <tabemann> right now I'm running on Cortex-M7, specificially STM32F746
16:08:23 <cbridge_> <tabemann> anyways, it works when I do this
16:09:31 <cbridge_> <NieDzejkob> does your implementation use any variables? perhaps it's non-reentrant
16:09:45 <cbridge_> <NieDzejkob> do your interrupt handlers use do-loops?
16:10:07 <cbridge_> <tabemann> my LOOP implementation does not use variables
16:10:42 <cbridge_> <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
16:12:17 <cbridge_> <tabemann> also, my LOOP counter and end are stored on the rstack, not in registers
16:12:30 <cbridge_> <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
16:12:50 <cbridge_> <NieDzejkob> and then inside your test loop, as soon as your state gets corrupted, read that global and print it
16:13:37 --- join: joanna_ joined #forth
16:14:31 <cbridge_> <tabemann> I know what code is being interrupted, that's the thing
16:14:55 <cbridge_> <tabemann> my big question is why is it corrupting it very infrequently
16:16:31 <cbridge_> <NieDzejkob> well maybe it only happens during a 2-instruction window
16:16:47 <cbridge_> <tabemann> and also, it's corrupting both the data stack and the rstack
16:17:10 <cbridge_> <tabemann> which makes me think it's actually corrupting registers, not memory
16:17:20 <cbridge_> <NieDzejkob> do interrupts run on their own stacks?
16:17:27 <cbridge_> <tabemann> nope
16:18:16 <cbridge_> <NieDzejkob> perhaps there's a moment where a stack read or write is incomplete, so the interrupts overwrite the top slot?
16:18:43 <cbridge_> <NieDzejkob> did you post your implementation of the relevant words here yet?
16:18:53 <cbridge_> <tabemann> IIRC aligned word accesses are atomic
16:18:59 <cbridge_> <tabemann> nope
16:19:29 <cbridge_> <NieDzejkob> any reason not to?
16:20:52 <cbridge_> <tabemann> https://dpaste.org/dmFj#L
16:22:39 <cbridge_> <tabemann> https://dpaste.org/4kXr
16:24:26 <cbridge_> <tabemann> I didn't realize there's both a dpaste.org and dpaste.com...
16:25:20 <cbridge_> <tabemann> anyways
16:27:20 --- quit: cbridge_ (Connection closed)
16:38:39 --- quit: joanna_ (Ping timeout: 120 seconds)
16:45:10 --- join: joanna_ joined #forth
16:53:39 --- quit: joanna_ (Ping timeout: 120 seconds)
18:00:33 --- join: joanna_ joined #forth
18:18:44 --- quit: joanna_ (Connection closed)
18:59:34 --- join: cbridge_ joined #forth
19:08:41 <cbridge_> <siraben> Mat9: the post was just about some surprising things that happen when one translate classical mathematics into a constructive setting
19:09:06 <cbridge_> <siraben> for CS and program verification, there isn't much of an issue because CS is almost all constructive anyway
19:10:24 <cbridge_> <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
19:10:57 <cbridge_> <siraben> factorial defined as: 1 begin over O= not while factorial_body repeat swap drop
19:11:20 <cbridge_> <siraben> s/translate/translates
19:14:45 <cbridge_> <moon> Coq is waaaay over my head
19:14:53 <cbridge_> <moon> but neat
19:21:16 <cbridge_> <siraben> remexre: "Typed programs don't leak data" https://dodisturb.me/posts/2021-06-27-Typed-Programs-Dont-Leak-Data.html
19:22:25 <cbridge_> <siraben> And using the right framework, you can prove real programs (e.g. written in C) correct https://gist.github.com/siraben/bdc2aa9b4a8f197722411b334febeaa0
20:10:45 --- quit: cbridge_ (Quit: bye)
20:10:56 --- join: cbridge_ joined #forth
21:59:51 --- nick: proteusguy -> proteus-guy
22:48:33 --- join: rain3 joined #forth
23:59:59 --- log: ended forth/21.06.27