[Qemu-devel] TCG semantics

[Qemu-devel] TCG semantics

[E.Robbins]

Hello,
I having been looking for prior work on a formalised semantics for the TCG language. I have seen passing references, and wondered if anyone can provide any pointers?

If this is the wrong list for this question, apologies, please direct me elsewhere.

Best,
Ed

Re: [Qemu-devel] TCG semantics

[Stefan Hajnoczi]

[-- Attachment #1: Type: text/plain, Size: 507 bytes --]

On Thu, Feb 02, 2017 at 12:09:02PM +0000, E.Robbins wrote:
> I having been looking for prior work on a formalised semantics for the TCG language. I have seen passing references, and wondered if anyone can provide any pointers?
> 
> If this is the wrong list for this question, apologies, please direct me elsewhere.

This is the right list.  Welcome!

Have you seen tcg/README?  It describes the TCG ops.

If it's out of date or missing information, then improving the document
seems worthwhile.

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 455 bytes --]

Re: [Qemu-devel] TCG semantics

[Ed Robbins]

On 3 February 2017 14:46:15 GMT+00:00, Stefan Hajnoczi <stefanha@gmail.com> wrote:
>On Thu, Feb 02, 2017 at 12:09:02PM +0000, E.Robbins wrote:
>> I having been looking for prior work on a formalised semantics for
>the TCG language. I have seen passing references, and wondered if
>anyone can provide any pointers?
>> 
>> If this is the wrong list for this question, apologies, please direct
>me elsewhere.
>
>This is the right list.  Welcome!
>

Thanks!

>Have you seen tcg/README?  It describes the TCG ops.
>

Yes, but was hoping for something a bit more precise, with a memory model etc. However, it isn't too much work to build one from the readme.

>If it's out of date or missing information, then improving the document
>seems worthwhile.

It seems pretty good. I was surprised that call instructions can have arguments/return specified, and wonder if those are normally just empty, so that emulation of the target stack/registers just carries the args/return in the background. Otherwise TCG must be detecting the target's arguments/return for each call which would need a clever dataflow analysis, or to follow calling convention and just hope, right?

I also am not clear about the precise operation of the byte swap instruction, but guess it follows the x86 bswap semantics.

I expect I can answer these questions by looking at some TCG output or checking the code, though (I don't want to waste anyone's time with that).

Thanks,
Ed

Re: [Qemu-devel] TCG semantics

[Peter Maydell]

On 6 February 2017 at 10:14, Ed Robbins <er209@kent.ac.uk> wrote:
> It seems pretty good. I was surprised that call instructions can
> have arguments/return specified, and wonder if those are normally
> just empty, so that emulation of the target stack/registers just
> carries the args/return in the background. Otherwise TCG must be
> detecting the target's arguments/return for each call which would
> need a clever dataflow analysis, or to follow calling convention
> and just hope, right?

"target" is a tricky word here, because it's unclear whether it
means the guest or the host CPU architecture. Note that tcg/README
always means "TCG target" (ie host) when it says "target", as
per section 2.

The "call" instruction is a call to a host function, so the
only calling convention in play is the host OS's ABI. (This
is what we use for calling C helper functions to implement
more complex bits of the guest emulation.) We don't know or
care about the guest's calling convention, because TCG only
sees things at the level of guest instructions and registers.

> I also am not clear about the precise operation of the byte
> swap instruction, but guess it follows the x86 bswap semantics.

Er, there's more than one definition of how to do byteswaps?
These instructions just swap the bytes in the however-many-bytes
wide lump of data they're defined to operate on. (If the
value type is wider than that lump of data then the insns
are allowed to assume the high bytes are zeroes, ie undefined
result if they're not.) Happy to take patches for clarifying
the docs, though.

thanks
-- PMM

Re: [Qemu-devel] TCG semantics

[Ed Robbins]

On 6 February 2017 10:39:11 GMT+00:00, Peter Maydell <peter.maydell@linaro.org> wrote:
>On 6 February 2017 at 10:14, Ed Robbins <er209@kent.ac.uk> wrote:
>> It seems pretty good. I was surprised that call instructions can
>> have arguments/return specified, and wonder if those are normally
>> just empty, so that emulation of the target stack/registers just
>> carries the args/return in the background. Otherwise TCG must be
>> detecting the target's arguments/return for each call which would
>> need a clever dataflow analysis, or to follow calling convention
>> and just hope, right?
>
>"target" is a tricky word here, because it's unclear whether it
>means the guest or the host CPU architecture. Note that tcg/README
>always means "TCG target" (ie host) when it says "target", as
>per section 2.
>
>The "call" instruction is a call to a host function, so the
>only calling convention in play is the host OS's ABI. (This
>is what we use for calling C helper functions to implement
>more complex bits of the guest emulation.) We don't know or
>care about the guest's calling convention, because TCG only
>sees things at the level of guest instructions and registers.
>

Makes sense, thanks for clearing that up.

>> I also am not clear about the precise operation of the byte
>> swap instruction, but guess it follows the x86 bswap semantics.
>
>Er, there's more than one definition of how to do byteswaps?
>These instructions just swap the bytes in the however-many-bytes
>wide lump of data they're defined to operate on. (If the
>value type is wider than that lump of data then the insns
>are allowed to assume the high bytes are zeroes, ie undefined
>result if they're not.) Happy to take patches for clarifying
>the docs, though.
>

Maybe there's only one way it's done, but it's good to be clear on the precise operation.

Thanks,
Ed