armv8/VMSAv8-64 has huge table support with optional contiguous bit allowing mapping up to 16GB at a time [0] [1]. Which will result in (almost) no address translations on any practical amount of memory available today.
Likely the issue is between most user systems not configuring huge tables and developers not keen on using things they can't test locally. Though huge tables are prominent in single-app servers and game consoles spaces.
Then it will be too noisy or too slow to be useful due to too many intermediate states. The feature of TLA+ is that it forces you to greatly dumb down the code to be able to use it, so it's more of verifying an algorithm represented as visual graph blocks rather than verifying assembly instructions.
I understand the wish for a magic bullet to just verify already existing code, but I recon the answer to this is to verify code before it's even written.
Hmm well obviously I know this, and it's like that because doing it properly is so far unachievable. Problem is there's an uncontrolled step between the code being run and the code being verified. This means we only verify an artist's sketch of the thing we want to test.
Same here with v3 and now being flabbergasted that my "open" project is suddenly dead-ended. (Re)doing an alternative software for PCB v3 is definitely possible, it just runs into economics, at average hourly rate we would put into it it just cheaper to buy decent espresso machine and move on.
> it just runs into economics, at average hourly rate we would put into it it just cheaper to buy decent espresso machine and move on.
Ha! I never thought about it this way, you're probably right on the time cost. Although, while the Decent espresso app which runs on the android tablet front end is open source, the firmware running the machine itself is not (unless I'm wrong). But given you can talk to it over bluetooth I think it fits my concept of "good enough" as the protocol is implemented in the open source app and the firmware as it stands gives you all the control knobs required to produce any result.
That being said, the reason I even considered a rewrite is because I particularly enjoy these kinds of ridiculous firmware replacements. For example, I've investigated it for the possibility of using rust to do it, it would be quite a bit of work as I would have to probably contribute to the state of the art but I've wanted an excuse for an embedded rust project and the STM32F411 (what you get in V3 by default) seems like not a terrible chip to base it on.
Gagguino has switched to STM32U585 and it seems like it's also supported relatively well in the embedded rust ecosystem.
Some popular in inner city: Tanto strandbad, Långholmsbadet, Smedsuddsbadet, Fredhällsbadet, Kristinebergsbadet, Brunnsviksbadet. Plenty of folks swim during hot periods in summer.
Yes, we went to Tanto but considering how much water that Stockholm is surrounded with, I can’t say it’s very accessible. That is also the view of some friends living there.
If it's a beach that's appropriate for smaller kids you're after with shallow water, yes you probably have to go to the more prepared beaches with sand that has shallow water a bit out.
Many places in central Stockholm have been built out from natural beaches by claiming water so the water will be deep at those points (probably held quays that was used for transports before trucks took over), but even in many places like that nobody would bat an eye if someone took a non-nudist swim.
Apart from the extremes most local teens and upwards will find cliffs by the water, as mentioned not appropriate for smaller kids and seniors as it's adjacent to deep water but perfect otherwise.
Only on Android, for what it's worth; most "vanilla" Linux aarch64 linkers chose 64K defaults several years ago. But yes, most Android applications with native (NDK) binaries will need to be rebuilt with the new 16kb max-page-size.
C# has support for unsafe code / pointer arithmetic / memory pinning / unmanaged types [1]. Using them it's possible to write performant computations where needed.
Mostly integration, for example some library can only be configured via env variables, but a developer might want to configure it from with-in the app it's integrated into and used from.
Also, few weeks ago I found a use for them when trying to pass configuration from Java/Kotlin to C++ library to be used during static constructors (invoked during dlopen) on Android, because at that phase native code cannot call back to JVM.
I agree that would be a poor implementation, but the library could be loaded at runtime using dlopen or equivalent.
This issue with that “interface” is the environment is process global. If the library is being loaded dynamically (specifically for some task) it would seem that the parameters are local to that task and should be taken by some reentrent init method. Alternatively, the process could be forked and environment set in the child without concern for thread safety or polluting the environment (think of the children!).
100% agree for "read only" software, like scanning, diagnostics, etc.
Control software is much more involved topic, let me illustrate it with a scenario: one family member is non-techy but has an insulin pump, another family member is techy and likes to hack around, they made a change to the insulin pump software to "improve it", but by accident the change triggered insulin overdose at night during sleep and family member died. We have rules and regulations not just to have rules and regulations, we have rules and regulations because they are written in blood.
While advocating for ability to freely modifying any life dependant control software is a noble goal, in my opinion it's the wrong end to approach it, instead it would be more constructive if we as computer science industry figure out ways how to make software such as we don't kill people, how to "certify" it in self service fashion (validation passed == no-one will die), etc, it's no trivial and it feels this particular part of our industry is not as developed/main stream as compared to something like civil engineering. If we have easy ways to ensure that modifying software will not lead to death then it will be easier to change the legislation to enforce this freedom.
In your scenario, there's protection at a societal level: manslaughter/homicide law.
Obviously their intent, the jurisdiction, their training/knowledge, and what sort of changes they attempted would matter in terms of how they were charged, prosecuted, etc.
If the device manufacturer updates software and injures or kills someone, they're liable on a criminal and/or civil level.
Before anyone starts rambling about how "they'll just calculate out their liability vs cost of proper software engineering blah blah"...in a civil lawsuit, at least in the US, the punitive portion of damages is for the express purpose of penalizing the defendant for shitty behavior, beyond actual damages, to discourage them and others from doing such a thing again.
McDonalds was slammed hard in the infamous coffee-scald case with a huge punitive portion. Before suing, the victim asked merely for medical expenses - nothing for the (enormous) pain and suffering from her genital burns. McDonalds told her to fuck off.
The jury was (to put it mildly) enraged on a number of counts: McD's knew their coffee was served well above industry standard temperatures, knew they'd injured people, and refused a reasonable request for damages.
Given that, having medical software be FLOSS certainly seems like it's a necessary step. Whether that alone is also sufficient is something that might warrant further debate.
Eg. in the opposing quadrant: maybe the insulin pump has a bug, but the new fix doesn't get certified in time and now the family member dies while their kin stands by whilst wringing their hands. This bears balancing.
I think -partially- this would fall under a patient's right[1] to choose an alternative treatment option, when presented with the pros and cons. A patient should be allowed to take considered risks.
I agree with it being the wrong way to go about it- I think the article fails to recognize that relying on the software being free isn't a solid enough certification of the software being appropriately safe to control a person's health. There has to be some other safeguard put in place- I'm not sure if it's legislation, but allowing a software update to break an app used by the elderly is unacceptable.
Updating the software should be done by qualified medical software engineers. Just like you wouldn't let a random untrained family member do surgery on you or prescribe you any drug. The free software aspect would still benefit the community, and people won't be on the fate of 1 company. If the company stops supporting the software, you could go to a medical software service company that has in-house experts on helping users with deprecated medical devices. That would at least be possible with free software, not with proprietary.
AFAIK Android updates are not as fast as they could be due to need for mobile operators to re-certify every update as the OS blob contains modem firmware. Apple is able to update iOS faster because modem firmware is separate from the rest of iOS. Hence having open source drivers in the kernel will not improve the situation much.
Likely the issue is between most user systems not configuring huge tables and developers not keen on using things they can't test locally. Though huge tables are prominent in single-app servers and game consoles spaces.
- [0] https://docs.kernel.org/arch/arm64/hugetlbpage.html - [1] https://developer.arm.com/documentation/ddi0487/latest (section D8.7.1 at the time of writing)