2
$\begingroup$

The universal Turing machine is the standard theoretical model of a stored-program computer. While in one sense as general as possible (Turing completeness), it doesn't explicitly contain many of the more advanced features of real-world/practical stored-program computers and their operating systems that have been developed since the 1950's. I am referring to basic features such as,

  • the fact that there is an "operating system" at all that can control execution of other stored-programs.

  • that there is a distinction between kernel and user mode, that the kernel mode can allocate and remove privileges to programs, and that this is hardcoded into the CPU,

  • That programs can execute "system calls" and that this causes a switch to kernel mode and to the OS,

  • the notion of "interactive programs", such as a shell with a command line where the input and output strings interact with some non-deterministic entity such as a human,

  • multi-programming,

  • the notion of CPU "interrupts" that can stop the execution of programs based on events,

  • etc.

I know this is a general question, but I am wondering whether there are mathematical models of computation that capture more advanced features such as these. I'm hoping someone could point me in the right direction.

Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ I don't think you can effectively and efficiently capture those ideas with abstract mathematical models. TMs are complicated enough, so introducing these concepts will prove to be extremely hard. That being said, there are different mathematical models that are capable of talking of other high-level ideas in programming languages, such as concurrency, memory safety, and more. $\endgroup$
    – nir shahar
    Commented Oct 15, 2021 at 16:42
  • $\begingroup$ @nirshahar, actually one of the motivations for my question is that I think it'd be clarifying to see an as-simple-as-possible mathematical formulation of some of these things. Mathematical models are often much more simple than their real-world engineered counterparts. I fully expect them to be complicated compared to TM's but I'm ok with that. $\endgroup$
    – user56834
    Commented Oct 15, 2021 at 17:27
  • 1
    $\begingroup$ The third bullet seems out of place. Shells are completely ordinary processes; there's nothing about them that would merit special treatment in a model. They often attach to a pty or Windows console, and those have some special treatment at the OS level (i.e. they aren't quite pipes), but it doesn't seem like a very interesting thing to model abstractly. $\endgroup$
    – benrg
    Commented Oct 15, 2021 at 19:16
  • $\begingroup$ @benrg, I was just giving it in contrast to a program that receives a fixed input and then runs, i.e. non-interactively, and a simple version of it. A GUI window would be another example of an interactive process (i.e. with a continual IO feedback loop), but maybe a purely text-based one is simple to model. $\endgroup$
    – user56834
    Commented Oct 15, 2021 at 19:29
  • $\begingroup$ @user56834 Any program that reads files is interactive when it reads files as those files could be typed out by hand with reading being blocked when at the end of the currently written part. $\endgroup$
    – worldsmithhelper
    Commented Oct 16, 2021 at 10:19

2 Answers 2

Reset to default
4
$\begingroup$

Formal verification deals with checking that software and hardware systems are correct by defining mathematical models that capture the behaviour of such systems. This is a large and active area, spanning verification of (components of) real-world hardware, operating systems, software, communication and security protocols, etc. All of these are modeled mathematically, so if you look them up, you will see what people are doing (and they are doing a lot).

Perhaps one lesson to be learned is that mathematical modeling of real-world systems need not proceed by defining one monolithic mathematical model that aims to describe every aspect of a given system – even if we could do that, it would not be terribly useful. Instead, it is much more useful to develop methods and techniques for building mathematical models, and then have many, many models, each suited to whatever aspect of a system we wish to study.

I can mention two examples (and you can google "formally verified X" for more):

  • CompCert - a formally verified C compiler, a high-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.

  • Verve - an operating system that is formally verified to be type safe

But yes, there's a whole industry of mathematical models for real-world hardware and software systems.

Improve this answer
$\endgroup$
0
$\begingroup$

  • The Computer Science answer is yes, the Turing machine can tick all the boxes of your list, except the last one.

  • The fact is that the functionality of parallel architectures can be emulated on purely sequential architectures, albeit at a very slow speed. A real world example for this is simulating and debugging a CUDA program on a CPU.

  • In practice, the Finite State Machine is the true computational model of any real computer system, i.e. a computer with finite memory. The finite state machine can model arbitrarily complex behaviour. Finite State Machines can model both software and hardware.

  • In digital hardware design, the FSM+Datapath model is the commonly used abstraction of complex digita hardware. See Why did finite-state controller with datapath win? for a discussion on this.

  • Privilege levels can be easily modeled using finite state machines.

  • In the semiconductor industry, a C++ library called SystemC is often used for modelling System-On-Chips and digital electronic subsystems. SystemC supports many types of abstract models.

  • TLM is a library in SystemC that stands for Transaction Level Models, and is widely used for early design state space exploration.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.