[ / / / / / / / / / / / / / ] [ dir / abdl / acme / agatha2 / animu / arepa / leftpol / tacos / vg ]

/tech/ - Technology

Email
Comment *
File
Password (Randomized for file and post deletion; you may also set your own.)
* = required field[▶ Show post options & limits]
Confused? See the FAQ.
Flag
Oekaki
Show oekaki applet
(replaces files and can be used instead)
Options

Allowed file types:jpg, jpeg, gif, png, webm, mp4, pdf
Max filesize is 16 MB.
Max image dimensions are 15000 x 15000.
You may upload 3 per post.


File: 6f5485205ff6d68⋯.jpg (51.66 KB, 1280x720, 16:9, sel4.jpg)

 No.969155

What is /tech/'s ideal operating system? We know it will use the superior sel4 microkernel. What else will it have? What filesystem? What shells? Will it be POSIX compliant, or will it be entirely different? What shell(s) will it have? Let's relax and LARP a little.

 No.969158

>>969155

Daily reminder that "proving code correct" means proving a relationship between a particular specification and an implementation, in no way meaning the specification has anything to do with the reality of the system. In many cases the specification is LARGER than the implementation.


 No.969159

You said shells twice. It would have a shell based on a "memelang" like a lisp or forth. Forth is often used as a shell on embedded systems.


 No.969162

>kernel

Something based on L4, indeed.

>filesystem

Something like XFS with self-healing properties would be nice. Leave volume management, raid management, compression on deduplication out of it.

>shell

I'm partial to sh with some of the most popular features/fixes of bash/zsh/ksh implemented. Getting out of the quoting hell might be nice too (arrays kind of solve it, though).

>POSIX

Provides a compatibility layer while fixing and improving the whole mess.


 No.969173

>>969159

>Forth is often used as a shell on embedded systems.

It's not used "as" a "shell", there's no shell, and it's not imitating the shell that isn't there.


 No.969174

>>969173

You do realize the bash shell is just a shitty programming language right.


 No.969179

>>969155

sel4 or microkernel-ified openbsd modified for an (obviously managed) pan-network memory address space so that multiple computers can be wrapped in one OS. In this sense, it would probably be more of a meta-os.

The filesystem would probably be HAMMER2 or ZFS. Otherwise, it would probably need to be custom-written.

Shells would be the same as most systems. There would need to be modifications to accommodate for the distributed nature of the OS.


 No.969194

>>969179

>microkernel-ified openbsd

I thought the BSD's already used microkernels. I thought that was one of their main selling points?


 No.969195

>>969194

Not at all. The only real microkernel OS out there that anyone uses is QNX.


 No.969201

Gentoo < Arch < Ideal OS > ReactOS > Windows > Ghetto SBC > OSX > Fridge


 No.969202

>>969195

OKL4 is more used than QNX will ever be, m8.


 No.969205

>>969202

I used QNX for a few years. It was reasonably supported.


 No.969221

Say this in the seL4 manual, can someone explain this to an OS noob? This sounds like the opposite of what should work?

>There are no arbitrary resource limits in the kernel apart from those dictated by the hardware and so many denial-of-service attacks via resource exhaustion are avoided.

This seems like it would delay resource exhaustion at best?


 No.969223

>>969202

OKL4 is a hypervisor you fuckwit. Your VM runner does not count as the base of an OS.


 No.969224

>>969221

>This seems like it would delay resource exhaustion at best?

Yes anon your hardware is not literally infinite. What the fuck do you expect.


 No.969228

>>969224

Avoid is different than delay. Avoid means it won't happen. Delay means it will just happen later than compared to other operating systems.


 No.969296

File: 8d7c1d9219a71fc⋯.pdf (648.62 KB, nelson-hyperkernel.pdf)

>>969155

But that already exists, anon. It's called genode.

Terry's TempleOS is not bad as well.

>>969195

I've used it, its main drawback is being proprietary and lack of drivers.


 No.969411

>>969221

It means that a userspace program (which in a microkernel architecture is basically everything) can't starve the kernel for resources and disrupt the system. In Linux and other OSs its possible under some conditions to consume more and more system resources until a kernel panic or system crash occurs.

Docker is an example of a program which does this, if the application running in a docker container logs to stdout the docker daemon will leak memory until there are no more free resources available and the system crashes.

>>969155

An ideal operating system would be microkernel based but the userspace applications will be run with a thin wrapper which translates the system calls so that the underlying microkernel can be anything rather than a specific microkernel. The wrapper will also be dynamic so that critical aspects of the system such as drivers and the filesystem can be easily swapped out, even while the system is running, without having to modify the applications. For god mode you can also have all the userspace applications distributed as LLVM intermediate code and then JIT them at runtime.

In terms of POSIX compliance probably not, POSIX is actually a bottleneck in highly concurrent systems and a few proposals for replacements exist. The UNIX style shell works and most people are familiar with it.


 No.969419

>>969155

I'd prefer Minix over seL4 since it has real world use on millions of machines.


 No.969427

Genode, ZFS, Qubes like interface/VMs sel4 kernel, Power9 or Riscv arch


 No.969429

>>969427

Why would you need a Qubes-like interface with VMs if you have a Genode system built on seL4?

Why not just use pure userspace programs on Genode?


 No.969431

Probably something like Qubes with a "microkernel" of sorts (while we're dreaming, I'd like it to be written in Ada). Theo says virtualization is buggy and exploitable, but I'd like to see him crack into a Qubes system. Until then, I'll believe virtualization is more secure than bare-metal.


 No.969446

>>969419

Minix probably wouldn't be terrible, but the drivers need some serious retooling to make anything useful for general computing.

>>969431

sek4 can be used as a hypervisor, and there's plans to make a qubes fork with it instead of xen.


 No.969447

>>969429

to run other OSs when needed


 No.969509

>>969201

What if we can make reactOS become arch's subsystemd?


 No.969652

File: 45357d6381628bc⋯.jpg (59.31 KB, 700x646, 350:323, 45357d6381628bc3546f402f82….jpg)


 No.969664

>>969411

> POSIX is actually a bottleneck in highly concurrent system

Care to elaborate?


 No.969772

>>969202

QNX is used in over 20,000,000 automobiles.


 No.969816

>>969155

this thread is the most cringeworthy buzzword salad i have ever read in my life


 No.969870


 No.969871


 No.969995

>>969411

>An ideal operating system would be microkernel based but the userspace applications will be run with a thin wrapper which translates the system calls so that the underlying microkernel can be anything rather than a specific microkernel. The wrapper will also be dynamic so that critical aspects of the system such as drivers and the filesystem can be easily swapped out, even while the system is running, without having to modify the applications. For god mode you can also have all the userspace applications distributed as LLVM intermediate code and then JIT them at runtime.

i came


 No.970265

>>969446

>sek4 can be used as a hypervisor, and there's plans to make a qubes fork with it instead of xen

Assume you meant sel4 here, but source pls. Can sel4 run on POWER9?


 No.970405

>>970265

what plans? where?


 No.970442

>>969995

People are actually already doing something like this with POSIX compatibility. Most POSIX compliant programs can make syscalls that either the linux, openbsd, or net/freebsd kernels can interpret. Since userspace calls for linux never change, only the internal kernel system calls, someone should implement the userland GNU/linux system calls as a translation layer for a intermediatary which you can then fork and fill in with your own custom kernel. Like you could run windows NT under it if you so wished *why would you ever do this?**. Or you could port SEL4 to the intermidiatary. To make all the userland code a LLVM intermidiatary would be trivial to do on the fly. Then you just need to write a super secure/performant JIT compiler.




[Return][Go to top][Catalog][Nerve Center][Cancer][Post a Reply]
Delete Post [ ]
[]
[ / / / / / / / / / / / / / ] [ dir / abdl / acme / agatha2 / animu / arepa / leftpol / tacos / vg ]