[M3devel] time conversion problems : Date.ToTime on AMD64_LINUX

Daniel Alejandro Benavides D. dabenavidesd at yahoo.es
Mon Apr 11 18:28:45 CEST 2011


Hi all:
although my understanding of the problem is not that good, I think there are two routes for this abstract way one could try to prove the correctness of some implementation by setting directly instrumention code to try to see for your self dynamically if you may that or what you want to see:
http://www.youtube.com/watch?v=zIgu9q0vVc0#t=2m06s

This could would run with just 3 missing modules from this sources besides their examples, maybe another time the HP guys allow us to see their works on that:
http://www.cs.arizona.edu/~collberg/Research/Modula-3/m3sources/html/zeus3D/

This package is missing from public repositories Elego too as I know, though they were in (see bottom links dead as of now, but, ... maybe you can look for yourselves):
http://www.cs.arizona.edu/~collberg/Research/Modula-3/

I know some ESC/Modula-3 tries to make some inferencing of invariants, but as I said it dones't mean this is totally computable, im fact in general its isn't, but it would be good to try.

Essentially where are the codes for showing that, or are you implementing this as private code?

Thanks in advance

--- El lun, 11/4/11, Mika Nystrom <mika at async.caltech.edu> escribió:

> De: Mika Nystrom <mika at async.caltech.edu>
> Asunto: Re: [M3devel] time conversion problems : Date.ToTime on AMD64_LINUX
> Para: "Jay K" <jay.krell at cornell.edu>
> CC: m3devel at elegosoft.com
> Fecha: lunes, 11 de abril, 2011 04:01
> I'm not sure about impossible. 
> But maybe...
> 
> Here's the situation.
> 
> I'm using unix time in my code.  Sometimes it needs to
> run on Windows.
> Some versions of Modula-3 on Windows use the Windows epoch
> for timekeeping.
> So I first request the time at midnight UTC Jan 1 1970 and
> set that to 
> "UnixEpoch".  On Unix systems I expect it to be zero,
> on some other systems
> it might be another number.
> 
> Now I've found what the problem is, and it's not anything
> you have done.
> In fact PM3 exhibits the same problem if you set everything
> up precisely
> the same.
> 
> The issue is that the server I am using is located in the
> United Kingdom
> and it has its time zone set to Europe/London. 
> Nowadays the Brits use the
> following definitions for time: 
> 
> in winter "Greenwich Mean Time" abbrev. "GMT" = UTC + 0
> in summer "British Summer Time" abbrev. "BST" = UTC + 3600
> 
> However, between October 26, 1968 and October 31, 1971,
> they used something
> else, to wit:
> 
> all year "British Standard Time" abbrev. "BST" = UTC +
> 3600
> 
> Note the confusing abbreviations.  British Standard
> Time (which no longer
> exists) and British Summer Time have the same
> abbreviation.  You might think
> this is sensible, because British Summer Time has the same
> value as British
> Standard Time (when the former is defined).
> 
> There is just one problem.  British Standard Time is
> not a "daylight
> savings time" whereas British Summer Time *is*. 
> Witness the output of
> zdump for London:
> 
> Europe/London  Sun Mar 19 02:00:00 1967 UTC = Sun Mar
> 19 03:00:00 1967 BST isdst=1 gmtoff=3600
> Europe/London  Sun Oct 29 01:59:59 1967 UTC = Sun Oct
> 29 02:59:59 1967 BST isdst=1 gmtoff=3600
> Europe/London  Sun Oct 29 02:00:00 1967 UTC = Sun Oct
> 29 02:00:00 1967 GMT isdst=0 gmtoff=0
> Europe/London  Sun Feb 18 01:59:59 1968 UTC = Sun Feb
> 18 01:59:59 1968 GMT isdst=0 gmtoff=0
> Europe/London  Sun Feb 18 02:00:00 1968 UTC = Sun Feb
> 18 03:00:00 1968 BST isdst=1 gmtoff=3600
> Europe/London  Sat Oct 26 22:59:59 1968 UTC = Sat Oct
> 26 23:59:59 1968 BST isdst=1 gmtoff=3600
> Europe/London  Sat Oct 26 23:00:00 1968 UTC = Sun Oct
> 27 00:00:00 1968 BST isdst=0 gmtoff=3600
> Europe/London  Sun Oct 31 01:59:59 1971 UTC = Sun Oct
> 31 02:59:59 1971 BST isdst=0 gmtoff=3600
> Europe/London  Sun Oct 31 02:00:00 1971 UTC = Sun Oct
> 31 02:00:00 1971 GMT isdst=0 gmtoff=0
> Europe/London  Sun Mar 19 01:59:59 1972 UTC = Sun Mar
> 19 01:59:59 1972 GMT isdst=0 gmtoff=0
> Europe/London  Sun Mar 19 02:00:00 1972 UTC = Sun Mar
> 19 03:00:00 1972 BST isdst=1 gmtoff=3600
> Europe/London  Sun Oct 29 01:59:59 1972 UTC = Sun Oct
> 29 02:59:59 1972 BST isdst=1 gmtoff=3600
> 
> The following lines are the special ones:
> 
> Europe/London  Sat Oct 26 22:59:59 1968 UTC = Sat Oct
> 26 23:59:59 1968 BST isdst=1 gmtoff=3600
> Europe/London  Sat Oct 26 23:00:00 1968 UTC = Sun Oct
> 27 00:00:00 1968 BST isdst=0 gmtoff=3600
> Europe/London  Sun Oct 31 01:59:59 1971 UTC = Sun Oct
> 31 02:59:59 1971 BST isdst=0 gmtoff=3600
> 
> Note how the gmtoff stays the same but isdst changes. 
> And this of course 
> straddles the definition of Unix time at Jan 1 1970
> 00:00:00 UTC.
> 
> Clearly there is a bug in M3's date code here.  I just
> don't understand what
> invariant the original author appealed to when he inserted
> the dst-changing code.
> It is hardly unusual for a given locale to have changed
> time zone rules...
> it is completely wrong for that to affect the conversion of
> times for a *different*
> locale (here I am just trying to do a time conversion for
> UTC, it shouldn't
> matter what country my computer is in when it does that!)
> 
>      Mika
> 
> Jay K writes:
> >--_2ede827e-b296-47fe-88ba-2c08d419ca54_
> >Content-Type: text/plain; charset="iso-8859-1"
> >Content-Transfer-Encoding: quoted-printable
> >
> >
> >This stuff is tricky. Maybe impossible. And requires a
> fair amount of time =
> >and attention.
> >Which I might not have right now=2C but which I
> definitely tried to apply a=
> >t the time.
> >
> >Can you compare with some historical versions?
> >e.g.
> >
> >http://modula3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-libs/m3core/src/time=
> >/POSIX/DatePosix.m3?rev=3D1.1.1.2=3Bcontent-type=3Dtext%2Fplain
> >http://modula3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-libs/m3core/src/time=
> >/POSIX/TimePosix.m3?rev=3D1.1.1.1=3Bcontent-type=3Dtext%2Fplain
> >
> >
> >and notice:
> >
> >http://modula3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-libs/m3core/src/time=
> >/POSIX/TimePosix.m3
> >Revision 1.3: download - view: text=2C markup=2C
> annotated - select for dif=
> >fs
> >Note: This also fixes the UTC timezone on Solaris=2C
> Interix=2C HP-UX=2C Cy=
> >gwin=2C which appear to have been historically broken.
> >
> >
> >I'm usually a bit nervous when I make accusations of
> long-term breakage.
> >
> >
> >And yeah there is a general problem of determining when
> daylight savings is=
> > in effect.
> >The rules very often change. The operating system needs
> a lot of data to kn=
> >ow this.
> >
> >
> >This stuff should be easy to debug without m3gdb.
> >Just print stuff to stdout liberally.
> >
> >Aha=2C see here:
> >http://modula3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-libs/m3core/src/time=
> >/POSIX/Attic/DateBsd.m3?rev=3D1.1.1.2=3Bcontent-type=3Dtext%2Fplain
> >
> >  (* adjust result to reflect "d.offset" *)
> >    EVAL Utime.time(ADR(now))=3B
> >    local_now :=3D
> Utime.localtime(ADR(now))=3B
> >    IF local_now.tm_isdst > 0 THEN
> >      (* decrement the local time zone
> by one hour if DST is in effect *)
> >      DEC(local_now.tm_gmtoff=2C 1 *
> SecsPerHour)
> >    END=3B
> >
> > - Jay
> >
> >> To: m3devel at elegosoft.com=3B
> jay.krell at cornell.edu
> >> Date: Sun=2C 10 Apr 2011 15:45:16 -0700
> >> From: mika at async.caltech.edu
> >> Subject: [M3devel] time conversion problems :
> Date.ToTime on AMD64_LINUX
> >>=20
> >> Hello m3devel (especially Jay)=2C
> >>=20
> >> I'm having some time conversion problems.  I
> *believe* (a bit hard to
> >> verify because m3gdb isn't working!!) that
> Date.ToTime called on
> >> Jan 1 1970 in timezone "UTC" or "GMT" is returning
> -3600 for me.
> >>=20
> >> I note the following (fairly recent) code in
> DatePosixC.c:
> >>=20
> >> #ifdef _TIME64_T
> >>     t =3D
> mktime64(&tm)=3B
> >> #else
> >>     t =3D mktime(&tm)=3B
> >> #endif
> >> #ifdef DATE_BSD
> >>     if (t =3D=3D -1)
> >>         goto
> Exit=3B
> >>=20
> >>     /* adjust result to
> reflect "date->offset" */
> >> #ifdef _TIME64_T
> >>     time64(&now)=3B
> >>     local_now =3D
> localtime64(&now)=3B
> >> #else
> >>     time(&now)=3B
> >>     local_now =3D
> localtime(&now)=3B
> >> #endif
> >>     assert(local_now !=3D
> NULL)=3B
> >>     if (local_now->tm_isdst
> > 0)
> >>       /* decrement the
> local time zone by one hour if DST is in effect */
> >>   
>    local_now->m3_tm_gmtoff -=3D
> SecsPerHour=3B
> >>=20
> >>     /* As above=2C we must
> negate "date->offset" to account for the
> >>        opposite sense of that
> field compared to Unix. */
> >>     t -=3D ((-date->offset)
> - local_now->m3_tm_gmtoff)=3B
> >> Exit:
> >> #endif
> >>     return t=3B
> >>=20
> >>=20
> >> What I don't understand is the subtracting off of
> SecsPerHour if
> >> "now" is DST.  Yeah=2C now is DST (it's
> April)=2C but the time I'm
> >> converting was in the winter=2C and besides GMT
> and UTC don't even
> >> have DST.=20
> >>=20
> >> I don't understand the intent of the code.. can
> someone explain why
> >> we're subtracting off an hour?  And why is it
> based on the value of=20
> >> tm_isdst of the *current* time?  Some
> additional documentation within
> >> the file would be helpful too.
> >>=20
> >> Note my conversion returns the correct 0 on
> various other M3
> >> implementations.
> >>=20
> >> Note the system time on my system is in a timezone
> that has DST=20
> >> (namely=2C BST) but I have changed the TZ
> environment variable to UTC or =
> >GMT
> >> before calling this code.
> >>=20
> >>      Mika
> >    
>         
>           
>   =
> >
> >--_2ede827e-b296-47fe-88ba-2c08d419ca54_
> >Content-Type: text/html; charset="iso-8859-1"
> >Content-Transfer-Encoding: quoted-printable
> >
> ><html>
> ><head>
> ><style><!--
> >.hmmessage P
> >{
> >margin:0px=3B
> >padding:0px
> >}
> >body.hmmessage
> >{
> >font-size: 10pt=3B
> >font-family:Tahoma
> >}
> >--></style>
> ></head>
> ><body class=3D'hmmessage'>
> >This stuff is tricky. Maybe impossible. And requires a
> fair amount of time =
> >and attention.<br>Which I might not have right
> now=2C but which I definitel=
> >y tried to apply at the time.<br><br>Can
> you compare with some historical v=
> >ersions?<br>e.g.<br><br>http://modula3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3=
> >/m3-libs/m3core/src/time/POSIX/DatePosix.m3?rev=3D1.1.1.2=3Bcontent-type=3D=
> >text%2Fplain<br>http://modula3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-libs=
> >/m3core/src/time/POSIX/TimePosix.m3?rev=3D1.1.1.1=3Bcontent-type=3Dtext%2Fp=
> >lain<br><br><br>and
> notice:<br><br>http://modula3.elegosoft.com/cgi-bin/cvs=
> >web.cgi/cm3/m3-libs/m3core/src/time/POSIX/TimePosix.m3<br>Revision
> <b>1.3</=
> >b>: <a href=3D"http://modula3.elegosoft.com/cgi-bin/cvsweb.cgi/%7Echeckout%=
> >7E/cm3/m3-libs/m3core/src/time/POSIX/TimePosix.m3?rev=3D1.3=3Bcontent-type=
> >=3Dtext%2Fplain"
> class=3D"download-link">download</a> - view: <a
> href=3D"ht=
> >tp://modula3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-libs/m3core/src/time/P=
> >OSIX/TimePosix.m3?rev=3D1.3=3Bcontent-type=3Dtext%2Fplain"
> class=3D"display=
> >-link">text</a>=2C <a href=3D"http://modula3.elegosoft.com/cgi-bin/cvsweb.c=
> >gi/cm3/m3-libs/m3core/src/time/POSIX/TimePosix.m3?rev=3D1.3=3Bcontent-type=
> >=3Dtext%2Fx-cvsweb-markup"
> class=3D"display-link">markup</a>=2C <a
> href=3D"=
> >http://modula3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-libs/m3core/src/time=
> >/POSIX/TimePosix.m3?annotate=3D1.3">annotated</a>
> - <a href=3D"http://modul=
> >a3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-libs/m3core/src/time/POSIX/TimeP=
> >osix.m3?r1=3D1.3#rev1.3">select&nbsp=3Bfor&nbsp=3Bdiffs</a><br>Note:
> This a=
> >lso fixes the UTC timezone on Solaris=2C Interix=2C
> HP-UX=2C Cygwin=2C whic=
> >h appear to have been historically
> broken.<br><br><br>I'm usually a bit ner=
> >vous when I make accusations of long-term
> breakage.<br><br><br>And yeah the=
> >re is a general problem of determining when daylight
> savings is in effect.<=
> >br>The rules very often change. The operating system
> needs a lot of data to=
> > know this.<br><br><br>This stuff
> should be easy to debug without m3gdb.<br=
> >>Just print stuff to stdout
> liberally.<br><br>Aha=2C see here:<br>http://mo=
> >dula3.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-libs/m3core/src/time/POSIX/At=
> >tic/DateBsd.m3?rev=3D1.1.1.2=3Bcontent-type=3Dtext%2Fplain<br><br><pre> 
> (*=
> > adjust result to reflect "d.offset" *)<br> 
>   EVAL Utime.time(ADR(now))=3B=
> ><br>    local_now :=3D
> Utime.localtime(ADR(now))=3B<br>    IF
> local_now.tm_=
> >isdst &gt=3B 0 THEN<br>     
> (* decrement the local time zone by one hour i=
> >f DST is in effect *)<br>     
> DEC(local_now.tm_gmtoff=2C 1 * SecsPerHour)<=
> >br>   
> END=3B<br></pre><br>&nbsp=3B-
> Jay<br><br>&gt=3B To: m3devel at elegosof=
> >t.com=3B jay.krell at cornell.edu<br>&gt=3B
> Date: Sun=2C 10 Apr 2011 15:45:16 =
> >-0700<br>&gt=3B From: mika at async.caltech.edu<br>&gt=3B
> Subject: [M3devel] t=
> >ime conversion problems : Date.ToTime on
> AMD64_LINUX<br>&gt=3B <br>&gt=3B H=
> >ello m3devel (especially Jay)=2C<br>&gt=3B
> <br>&gt=3B I'm having some time =
> >conversion problems.  I *believe* (a bit hard
> to<br>&gt=3B verify because m=
> >3gdb isn't working!!) that Date.ToTime called
> on<br>&gt=3B Jan 1 1970 in ti=
> >mezone "UTC" or "GMT" is returning -3600 for
> me.<br>&gt=3B <br>&gt=3B I not=
> >e the following (fairly recent) code in
> DatePosixC.c:<br>&gt=3B <br>&gt=3B =
> >#ifdef _TIME64_T<br>&gt=3B 
>    t =3D
> mktime64(&amp=3Btm)=3B<br>&gt=3B #else=
> ><br>&gt=3B     t =3D
> mktime(&amp=3Btm)=3B<br>&gt=3B
> #endif<br>&gt=3B #ifdef=
> > DATE_BSD<br>&gt=3B 
>    if (t =3D=3D -1)<br>&gt=3B 
>        goto Exit=3B<br>=
> >&gt=3B <br>&gt=3B 
>    /* adjust result to reflect
> "date-&gt=3Boffset" */<br=
> >>&gt=3B #ifdef
> _TIME64_T<br>&gt=3B 
>    time64(&amp=3Bnow)=3B<br>&gt=3B 
>    =
> >local_now =3D
> localtime64(&amp=3Bnow)=3B<br>&gt=3B
> #else<br>&gt=3B     time=
> >(&amp=3Bnow)=3B<br>&gt=3B 
>    local_now =3D
> localtime(&amp=3Bnow)=3B<br>&gt=
> >=3B #endif<br>&gt=3B 
>    assert(local_now !=3D
> NULL)=3B<br>&gt=3B     if (l=
> >ocal_now-&gt=3Btm_isdst &gt=3B
> 0)<br>&gt=3B       /*
> decrement the local ti=
> >me zone by one hour if DST is in effect
> */<br>&gt=3B   
>    local_now-&gt=3B=
> >m3_tm_gmtoff -=3D SecsPerHour=3B<br>&gt=3B
> <br>&gt=3B     /* As above=2C
> we=
> > must negate "date-&gt=3Boffset" to account for
> the<br>&gt=3B        opposi=
> >te sense of that field compared to Unix.
> */<br>&gt=3B     t -=3D
> ((-date-&g=
> >t=3Boffset) -
> local_now-&gt=3Bm3_tm_gmtoff)=3B<br>&gt=3B
> Exit:<br>&gt=3B #e=
> >ndif<br>&gt=3B     return
> t=3B<br>&gt=3B <br>&gt=3B
> <br>&gt=3B What I don't=
> > understand is the subtracting off of SecsPerHour
> if<br>&gt=3B "now" is DST=
> >.  Yeah=2C now is DST (it's April)=2C but the time
> I'm<br>&gt=3B converting=
> > was in the winter=2C and besides GMT and UTC don't
> even<br>&gt=3B have DST=
> >. <br>&gt=3B <br>&gt=3B I don't
> understand the intent of the code.. can som=
> >eone explain why<br>&gt=3B we're subtracting
> off an hour?  And why is it ba=
> >sed on the value of <br>&gt=3B tm_isdst of
> the *current* time?  Some additi=
> >onal documentation within<br>&gt=3B the file
> would be helpful too.<br>&gt=
> >=3B <br>&gt=3B Note my conversion returns the
> correct 0 on various other M3=
> ><br>&gt=3B
> implementations.<br>&gt=3B <br>&gt=3B
> Note the system time on my=
> > system is in a timezone that has DST
> <br>&gt=3B (namely=2C BST) but I have=
> > changed the TZ environment variable to UTC or
> GMT<br>&gt=3B before calling=
> > this code.<br>&gt=3B
> <br>&gt=3B      Mika<br>
>    
>         
>        
> >      </body>
> ></html>=
> >
> >--_2ede827e-b296-47fe-88ba-2c08d419ca54_--
> 



More information about the M3devel mailing list