https://futureofcoding.org/ logo
Join Slack
Powered by
(Unavoidable) shared mutable state marks cooperati...
# thinking-together
p
(Unavoidable) shared mutable state marks cooperating objects + one’s data depends on the other’s (in time) for runtime branching. Could not we explicitly restrict the access of (lets say 2) objects (1-1 methods) in time - relative to one other? We could listen to all the relevant(!) messages to validate the access of objects for the shared state. The dev should enumerate 2 things (for each accessing method per mutable state): • All the valid sequences of messages which indicate access is granted for the method. “Synced.” • All the valid sequences of messages which indicate access is denied for the method. “Sync needed.” (Modelled with Finite Automatons) We should be also be able to determine (generate) all the relevant(!) sequences of messages (per state per accessing method) - and check if something is left out. If so, the system prompts us and we must fill put the remaining cases to “granted”/“denied”. (The general idea is to always EXPLICITLY enumerate when to do and when NOT to do something so we can later check with exhaustive search.) By relevant messages and relevant sequences of messages I mean those which by cascading through in the system (calls) might have any chance to effect the access of the method. Only if there are too many branches (combinatorial explosion) shall we narrow EXPLICITLY the cases we think behave the same. (By defining more Finite Automatons). I have this idea for a long time now and I come back to it over and over again. Seems really simple, but did not find anything like that yet. The closest findings are something like TLA+ and Temporal Logic (especially from the complexity of CTL), but to me this process seems quite good and I am not sure why it does not exists yet. @Kartik Agaram @Prathyush
k
Not following this at all.
p
Okay, I’ll try to rephrase it then.
w
same here
there are several languages that have features to only allow valid sequences of method calls, usually by changing an internal state machine or chaining of state.. it sound similar to what you're saying, but can't quite tell
👍 1
d
I are we talking about something like this? Synchronization is only a problem in programs which allow shared mutable state, and parallel execution. Get rid of one or the other, and suddenly you don't need synchronization mechanisms like locks, semaphores, mutexes, etc. It sounds like the topic is about using static code analysis to prove when code is not synchronous anyway, or otherwise under what conditions it isn't vulnerable to certain synchronization problems with shared mutable state. And having determined this, the compiler (or something else) can make some sort of guarantee or restriction or optimization or call it an error if synchronization mechanisms are not put in place, or something.
m
don't know if I follow, but isn't this related to session types? "In complex distributed systems communicating participants agree on a protocol to follow, specifying type and direction of data exchanged. •Session types are a type formalism used to model structured communication-based programming. •Guarantee privacy,communication safety and session fidelity"
❤️ 1
also pony's type system helps "Pony doesn’t have locks nor atomic operations or anything like that. Instead, the type system ensures at compile time that your concurrent program can never have data races. So you can write highly concurrent code and never get it wrong." https://www.ponylang.io
erlang makes it simpler, the code inside an actor in single threaded and the message inbox serializes messages sent to it so you don't have to lock anything, just use many actors and you take advantage of multiple cores
☝️ 1
p
@Mariano Guerra pony lang and session types are nice pointers, ty!
@Wouter valid sequences of method calls: yes exactly, I need this! Can you give me examples of languages doing that? I’d be curious!
w
Trying to remember the name of the language.. but failing 😞
p
@Wouter any other pointer? 😛
@Dan Cook “Synchronization is only a problem in programs which allow shared mutable state, and parallel execution. Get rid of one or the other, and suddenly you don’t need synchronization mechanisms like locks, semaphores, mutexes, etc.” Yes, that is totally true, but unfortunately I meant something a little bit different by “Synced” / “Synced needed.” 🙂 (I intentionally tried to omit the word synchronization, but the meaning I’ve been looking for is too similar…) Let me clarify. Earlier we had a discussion on the negative sides of FP and one point was something like “OO preserves identity, FP does not” @shalabh. The point is that you might get rid of shared mutable state but then to “preserve identity” you have to make it up “by hand”. No matter what, if there are 2 independent pieces of code (like objects) which both use the same piece of information (the same identity), then there must be some kind of “syncronization” which prevents the system to work on corrupt data (without sync). Sure, one option is using references to the same memory address, but then the two objects are not really independent but coupled. If they are truly independent then the syncronization of “their common state” must be embedded in their communication (protocol). The “protocol between communicating objects”/“mechanisms of the system” must ensure the sequences of events are valid between all objects. My idea is to define both 
valid
and 
invalid
sequences of messages in the system so we can check out if some sequence (pattern) is left out, because in theory we are able to generate all the different kinds of sequences - expressing them with patterns. This really seems like connecting state machines, but still I did not find a well-known project which uses something like that. My closest findings are 
xstate
library (Typescript) and some SAT solvers coming from the CTL branch of Temporary Logic.
s
I'm not sure I really get where you're going. When you say 'valid sequence' do you mean a sequence of messages that are absorbed by a single object? So each class/object defines what the valid sequence is? Another concern is that there are multiple possible valid sequences and timing may still come into play. E.g. 'push', 'push', 'pop', 'pop', vs 'push', 'pop', 'push', 'pop' are both valid sequences to a stack like object.
2 Views
Open in Slack
PreviousNext
Powered by